chore(data/polynomial): remove monomial_one_eq_X_pow (#4734)

monomial_one_eq_X_pow was a duplicate of X_pow_eq_monomial



Co-authored-by: faenuccio <65080144+faenuccio@users.noreply.github.com>

Author: faenuccio

src/data/polynomial/coeff.lean

@@ -86,7 +86,7 @@ add_monoid_algebra.mul_single_zero_apply p a n
 
 lemma coeff_X_pow (k n : ℕ) :
   coeff (X^k : polynomial R) n = if n = k then 1 else 0 :=
-by rw [← monomial_one_eq_X_pow]; simp [monomial, single, eq_comm, coeff]; congr
+by { simp only [X_pow_eq_monomial, monomial, single, eq_comm], congr }
 
 @[simp]
 lemma coeff_X_pow_self (n : ℕ) :

src/data/polynomial/eval.lean

@@ -59,7 +59,7 @@ end
 
 @[simp] lemma eval₂_X_pow {n : ℕ} : (X^n).eval₂ f x = x^n :=
 begin
-  rw ←monomial_one_eq_X_pow,
+  rw X_pow_eq_monomial,
   convert eval₂_monomial f x,
   simp,
 end

src/data/polynomial/monomial.lean

@@ -83,18 +83,9 @@ begin
   simpa only [and_true, eq_self_iff_true, or_false, one_ne_zero, and_self],
 end
 
-lemma monomial_one_eq_X_pow : ∀{n}, monomial n (1 : R) = X^n
-| 0     := rfl
-| (n+1) :=
-  calc monomial (n + 1) (1 : R) = monomial n 1 * X : by rw [X, monomial_mul_monomial, mul_one]
-    ... = X^n * X : by rw [monomial_one_eq_X_pow]
-    ... = X^(n+1) : by simp only [pow_add, pow_one]
-
 lemma monomial_eq_smul_X {n} : monomial n (a : R) = a • X^n :=
-begin
-  calc monomial n a = monomial n (a * 1) : by simp
-    ... = a • monomial n 1 : (smul_single' _ _ _).symm
-    ... = a • X^n  : by rw monomial_one_eq_X_pow
-end
+calc monomial n a = monomial n (a * 1) : by simp
+  ... = a • monomial n 1 : (smul_single' _ _ _).symm
+  ... = a • X^n  : by rw X_pow_eq_monomial
 
 end polynomial

src/ring_theory/polynomial_algebra.lean

@@ -208,7 +208,7 @@ begin
   { intros n a,
     rw [inv_fun, eval₂_monomial, alg_hom.coe_to_ring_hom, algebra.tensor_product.include_left_apply,
       algebra.tensor_product.tmul_pow, one_pow, algebra.tensor_product.tmul_mul_tmul,
-      mul_one, one_mul, to_fun_alg_hom_apply_tmul, ←monomial_one_eq_X_pow],
+      mul_one, one_mul, to_fun_alg_hom_apply_tmul, X_pow_eq_monomial],
     dsimp [monomial],
     rw [finsupp.sum_single_index]; simp, }
 end