feat(Polynomial): new lemmas and noncommutative generalizations (#19665)

In `Algebra/Polynomial/Eval/Degree.lean`: two new lemmas about the coefficients and zero-ness of the composition of a polynomial with `C r * X`.

Noncommutative generalizations:
`Algebra/Polynomial/Degree/Lemmas.lean`: two lemmas
`RingTheory/Polynomial/Tower.lean`: one lemma
`RingTheory/Polynomial/IntegralNormalization.lean`: add `of_commute` versions of two lemmas similar to [Polynomial.scaleRoots_eval₂_mul_of_commute](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Polynomial/ScaleRoots.html#Polynomial.scaleRoots_eval%E2%82%82_mul_of_commute) and generalize one lemma.

Mathlib/Algebra/Polynomial/Degree/Lemmas.lean

@@ -369,20 +369,16 @@ theorem leadingCoeff_comp (hq : natDegree q ≠ 0) :
 
 end NoZeroDivisors
 
-section CommRing
-variable [CommRing R] {p q : R[X]}
-
-@[simp] lemma comp_neg_X_leadingCoeff_eq (p : R[X]) :
+@[simp] lemma comp_neg_X_leadingCoeff_eq [Ring R] (p : R[X]) :
     (p.comp (-X)).leadingCoeff = (-1) ^ p.natDegree * p.leadingCoeff := by
   nontriviality R
   by_cases h : p = 0
   · simp [h]
   rw [Polynomial.leadingCoeff, natDegree_comp_eq_of_mul_ne_zero, coeff_comp_degree_mul_degree] <;>
-  simp [mul_comm, h]
-
-variable [IsDomain R]
+  simp [((Commute.neg_one_left _).pow_left _).eq, h]
 
-lemma comp_eq_zero_iff : p.comp q = 0 ↔ p = 0 ∨ p.eval (q.coeff 0) = 0 ∧ q = C (q.coeff 0) := by
+lemma comp_eq_zero_iff [Semiring R] [NoZeroDivisors R] {p q : R[X]} :
+    p.comp q = 0 ↔ p = 0 ∨ p.eval (q.coeff 0) = 0 ∧ q = C (q.coeff 0) := by
   refine ⟨fun h ↦ ?_, Or.rec (fun h ↦ by simp [h]) fun h ↦ by rw [h.2, comp_C, h.1, C_0]⟩
   have key : p.natDegree = 0 ∨ q.natDegree = 0 := by
     rw [← mul_eq_zero, ← natDegree_comp, h, natDegree_zero]
@@ -392,8 +388,6 @@ lemma comp_eq_zero_iff : p.comp q = 0 ↔ p = 0 ∨ p.eval (q.coeff 0) = 0 ∧ q
   · rw [key, comp_C, C_eq_zero] at h
     exact Or.inr ⟨h, key⟩
 
-end CommRing
-
 section DivisionRing
 
 variable {K : Type*} [DivisionRing K]

Mathlib/Algebra/Polynomial/Eval/Degree.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Kim Morrison, Jens Wagemaker
 -/
+import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import Mathlib.Algebra.Polynomial.Degree.Support
 import Mathlib.Algebra.Polynomial.Degree.Units
 import Mathlib.Algebra.Polynomial.Eval.Coeff
@@ -107,6 +108,21 @@ theorem coeff_comp_degree_mul_degree (hqd0 : natDegree q ≠ 0) :
   case h₁ =>
     simp +contextual
 
+@[simp] lemma comp_C_mul_X_coeff {r : R} {n : ℕ} :
+    (p.comp <| C r * X).coeff n = p.coeff n * r ^ n := by
+  simp_rw [comp, eval₂_eq_sum_range, (commute_X _).symm.mul_pow,
+    ← C_pow, finset_sum_coeff, coeff_C_mul, coeff_X_pow]
+  rw [Finset.sum_eq_single n _ fun h ↦ ?_, if_pos rfl, mul_one]
+  · intro b _ h; simp_rw [if_neg h.symm, mul_zero]
+  · rw [coeff_eq_zero_of_natDegree_lt, zero_mul]
+    rwa [Finset.mem_range_succ_iff, not_le] at h
+
+lemma comp_C_mul_X_eq_zero_iff {r : R} (hr : r ∈ nonZeroDivisors R) :
+    p.comp (C r * X) = 0 ↔ p = 0 := by
+  simp_rw [ext_iff]
+  refine forall_congr' fun n ↦ ?_
+  rw [comp_C_mul_X_coeff, coeff_zero, mul_right_mem_nonZeroDivisors_eq_zero_iff (pow_mem hr _)]
+
 end Comp
 
 section Map

Mathlib/RingTheory/Polynomial/IntegralNormalization.lean

@@ -115,24 +115,30 @@ theorem integralNormalization_degree : (integralNormalization p).degree = p.degr
   · rw [← degree_scaleRoots, ← integralNormalization_mul_C_leadingCoeff]
     exact (degree_mul_le _ _).trans (add_le_of_nonpos_right degree_C_le)
 
-variable [CommSemiring S]
+variable {A : Type*} [CommSemiring S] [Semiring A]
 
 theorem leadingCoeff_smul_integralNormalization (p : S[X]) :
     p.leadingCoeff • integralNormalization p = scaleRoots p p.leadingCoeff := by
   rw [Algebra.smul_def, algebraMap_eq, mul_comm, integralNormalization_mul_C_leadingCoeff]
 
-theorem integralNormalization_eval₂_leadingCoeff_mul (h : 1 ≤ p.natDegree) (f : R →+* S) (x : S) :
+theorem integralNormalization_eval₂_leadingCoeff_mul_of_commute (h : 1 ≤ p.natDegree) (f : R →+* A)
+    (x : A) (h₁ : Commute (f p.leadingCoeff) x) (h₂ : ∀ {r r'}, Commute (f r) (f r')) :
     (integralNormalization p).eval₂ f (f p.leadingCoeff * x) =
       f p.leadingCoeff ^ (p.natDegree - 1) * p.eval₂ f x := by
   rw [eval₂_eq_sum_range, eval₂_eq_sum_range, Finset.mul_sum]
   apply Finset.sum_congr
   · rw [natDegree_eq_of_degree_eq p.integralNormalization_degree]
   intro n _hn
-  rw [mul_pow, ← mul_assoc, ← f.map_pow, ← f.map_mul,
-    integralNormalization_coeff_mul_leadingCoeff_pow _ h, f.map_mul, f.map_pow]
-  ring
+  rw [h₁.mul_pow, ← mul_assoc, ← f.map_pow, ← f.map_mul,
+    integralNormalization_coeff_mul_leadingCoeff_pow _ h, f.map_mul, h₂.eq, f.map_pow, mul_assoc]
 
-theorem integralNormalization_eval₂_eq_zero {p : R[X]} (f : R →+* S) {z : S} (hz : eval₂ f z p = 0)
+theorem integralNormalization_eval₂_leadingCoeff_mul (h : 1 ≤ p.natDegree) (f : R →+* S) (x : S) :
+    (integralNormalization p).eval₂ f (f p.leadingCoeff * x) =
+      f p.leadingCoeff ^ (p.natDegree - 1) * p.eval₂ f x :=
+  integralNormalization_eval₂_leadingCoeff_mul_of_commute h _ _ (.all _ _) (.all _ _)
+
+theorem integralNormalization_eval₂_eq_zero_of_commute {p : R[X]} (f : R →+* A) {z : A}
+    (hz : eval₂ f z p = 0) (h₁ : Commute (f p.leadingCoeff) z) (h₂ : ∀ {r r'}, Commute (f r) (f r'))
     (inj : ∀ x : R, f x = 0 → x = 0) :
     eval₂ f (f p.leadingCoeff * z) (integralNormalization p) = 0 := by
   obtain (h | h) := p.natDegree.eq_zero_or_pos
@@ -141,20 +147,20 @@ theorem integralNormalization_eval₂_eq_zero {p : R[X]} (f : R →+* S) {z : S}
       simp [h0]
     · rw [eq_C_of_natDegree_eq_zero h, eval₂_C] at hz
       exact absurd (inj _ hz) h0
-  · rw [integralNormalization_eval₂_leadingCoeff_mul h, hz, mul_zero]
+  · rw [integralNormalization_eval₂_leadingCoeff_mul_of_commute h _ _ h₁ h₂, hz, mul_zero]
 
-end Semiring
-
-section CommSemiring
-
-variable [CommSemiring R] [CommSemiring S]
+theorem integralNormalization_eval₂_eq_zero {p : R[X]} (f : R →+* S) {z : S} (hz : eval₂ f z p = 0)
+    (inj : ∀ x : R, f x = 0 → x = 0) :
+    eval₂ f (f p.leadingCoeff * z) (integralNormalization p) = 0 :=
+  integralNormalization_eval₂_eq_zero_of_commute _ hz (.all _ _) (.all _ _) inj
 
-theorem integralNormalization_aeval_eq_zero [Algebra R S] {f : R[X]} {z : S} (hz : aeval z f = 0)
-    (inj : ∀ x : R, algebraMap R S x = 0 → x = 0) :
-    aeval (algebraMap R S f.leadingCoeff * z) (integralNormalization f) = 0 :=
-  integralNormalization_eval₂_eq_zero (algebraMap R S) hz inj
+theorem integralNormalization_aeval_eq_zero [Algebra S A] {f : S[X]} {z : A} (hz : aeval z f = 0)
+    (inj : ∀ x : S, algebraMap S A x = 0 → x = 0) :
+    aeval (algebraMap S A f.leadingCoeff * z) (integralNormalization f) = 0 :=
+  integralNormalization_eval₂_eq_zero_of_commute (algebraMap S A) hz
+    (Algebra.commute_algebraMap_left _ _) (.map (.all _ _) _) inj
 
-end CommSemiring
+end Semiring
 
 section IsCancelMulZero
 

Mathlib/RingTheory/Polynomial/Tower.lean

@@ -36,9 +36,9 @@ theorem aeval_map_algebraMap (x : B) (p : R[X]) : aeval x (map (algebraMap R A)
   rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]
 
 @[simp]
-lemma eval_map_algebraMap (P : R[X]) (a : A) :
-    (map (algebraMap R A) P).eval a = aeval a P := by
-  rw [← aeval_map_algebraMap (A := A), coe_aeval_eq_eval]
+lemma eval_map_algebraMap (P : R[X]) (b : B) :
+    (map (algebraMap R B) P).eval b = aeval b P := by
+  rw [aeval_def, eval_map]
 
 end Semiring