feat(RingTheory/PolynomialAlgebra): lemmas about X and C (#8294)

Mathlib/RingTheory/PolynomialAlgebra.lean

@@ -225,6 +225,23 @@ noncomputable def matPolyEquiv : Matrix n n R[X] ≃ₐ[R] (Matrix n n R)[X] :=
     (polyEquivTensor R (Matrix n n R)).symm
 #align mat_poly_equiv matPolyEquiv
 
+@[simp] theorem matPolyEquiv_symm_C (M : Matrix n n R) : matPolyEquiv.symm (C M) = M.map C := by
+  simp [matPolyEquiv, ←C_eq_algebraMap]
+
+@[simp] theorem matPolyEquiv_map_C (M : Matrix n n R) : matPolyEquiv (M.map C) = C M := by
+  rw [←matPolyEquiv_symm_C, AlgEquiv.apply_symm_apply]
+
+@[simp] theorem matPolyEquiv_symm_X :
+    matPolyEquiv.symm X = diagonal fun _ : n => (X : R[X]) := by
+  suffices (Matrix.map 1 fun x ↦ X * algebraMap R R[X] x) = diagonal fun _ : n => (X : R[X]) by
+    simpa [matPolyEquiv]
+  rw [←Matrix.diagonal_one]
+  simp [-Matrix.diagonal_one]
+
+@[simp] theorem matPolyEquiv_diagonal_X :
+    matPolyEquiv (diagonal fun _ : n => (X : R[X])) = X := by
+  rw [←matPolyEquiv_symm_X, AlgEquiv.apply_symm_apply]
+
 open Finset
 
 theorem matPolyEquiv_coeff_apply_aux_1 (i j : n) (k : ℕ) (x : R) :