feat(Algebra/Polynomial/Bivariate): more API for swap (leanprover-community#35974)

Author: justus-springer

Mathlib/Algebra/Polynomial/Bivariate.lean

@@ -247,6 +247,9 @@ def Bivariate.swap : R[X][Y] ≃ₐ[R] R[X][Y] := by
   apply AlgEquiv.ofAlgHom (aevalAeval (Y : R[X][Y]) (C X)) (aevalAeval (Y : R[X][Y]) (C X))
     <;> (ext n m <;> simp)
 
+@[simp]
+theorem Bivariate.swap_symm : swap.symm = (swap (R := R)) := rfl
+
 @[simp]
 theorem Bivariate.swap_apply (p : R[X][Y]) : swap p = p.aevalAeval (A := R[X][Y]) Y (C X) := rfl
 
@@ -259,12 +262,19 @@ theorem Bivariate.swap_C_C (r : R) : swap (C (C r)) = C (C r) := by simp
 theorem Bivariate.swap_C (f : R[X]) : swap (C f) = f.map C := by
   simpa [← algebraMap_eq] using aeval_X_left_eq_map f
 
+theorem Bivariate.swap_swap_apply (p : R[X][Y]) : swap (swap p) = p :=
+  AlgEquiv.symm_apply_apply swap p
+
 theorem Bivariate.swap_map_C (f : R[X]) : swap (f.map C) = C f := by
   induction f using Polynomial.induction_on' with
   | add => aesop
   | monomial n a => rw [map_monomial, ← C_mul_X_pow_eq_monomial, ← C_mul_X_pow_eq_monomial,
     map_mul, map_pow, swap_Y, C_mul, C_pow, Bivariate.swap_C_C]
 
+theorem Bivariate.swap_monomial (n : ℕ) (f : R[X]) :
+    swap (monomial n f) = f.map C * C (X ^ n) := by
+  simp [← C_mul_X_pow_eq_monomial, aeval_X_left_eq_map]
+
 theorem Bivariate.swap_monomial_monomial (n m : ℕ) (r : R) :
     swap (monomial n (monomial m r)) = (monomial m (monomial n r)) := by
   simp [← C_mul_X_pow_eq_monomial]; ac_rfl