feat(Algebra/Polynomial): small and useful lemmas (#29956)

Author: SnirBroshi

Mathlib/Algebra/Polynomial/AlgebraMap.lean

@@ -479,10 +479,9 @@ theorem isRoot_of_eval₂_map_eq_zero (hf : Function.Injective f) {r : R} :
   apply hf
   rw [← eval₂_hom, h, f.map_zero]
 
-theorem isRoot_of_aeval_algebraMap_eq_zero [Algebra R S] {p : R[X]}
-    (inj : Function.Injective (algebraMap R S)) {r : R} (hr : aeval (algebraMap R S r) p = 0) :
-    p.IsRoot r :=
-  isRoot_of_eval₂_map_eq_zero inj hr
+theorem isRoot_of_aeval_algebraMap_eq_zero [Algebra R S] [FaithfulSMul R S] {p : R[X]} {r : R}
+    (hr : p.aeval (algebraMap R S r) = 0) : p.IsRoot r :=
+  isRoot_of_eval₂_map_eq_zero (FaithfulSMul.algebraMap_injective _ _) hr
 
 end Semiring
 

Mathlib/Algebra/Polynomial/Basic.lean

@@ -459,6 +459,9 @@ theorem C_0 : C (0 : R) = 0 := by simp
 theorem C_1 : C (1 : R) = 1 :=
   rfl
 
+theorem C_ofNat (n : ℕ) [n.AtLeastTwo] : C ofNat(n) = (ofNat(n) : R[X]) :=
+  rfl
+
 theorem C_mul : C (a * b) = C a * C b :=
   C.map_mul a b
 

Mathlib/Algebra/Polynomial/Degree/Lemmas.lean

@@ -271,6 +271,39 @@ theorem natDegree_map_eq_iff {f : R →+* S} {p : Polynomial R} :
   · simp_rw [h, ne_eq, or_true, iff_true, ← Nat.le_zero, ← h, natDegree_map_le]
   simp_all [natDegree, WithBot.unbotD_eq_unbotD_iff]
 
+theorem degree_map_eq_of_isUnit_leadingCoeff [Nontrivial S] (f : R →+* S)
+    (hp : IsUnit p.leadingCoeff) : (p.map f).degree = p.degree :=
+  degree_map_eq_of_leadingCoeff_ne_zero _ <| f.isUnit_map hp |>.ne_zero
+
+theorem natDegree_map_eq_of_isUnit_leadingCoeff [Nontrivial S] (f : R →+* S)
+    (hp : IsUnit p.leadingCoeff) : (p.map f).natDegree = p.natDegree :=
+  natDegree_eq_natDegree <| degree_map_eq_of_isUnit_leadingCoeff _ hp
+
+theorem leadingCoeff_map_eq_of_isUnit_leadingCoeff [Nontrivial S] (f : R →+* S)
+    (hp : IsUnit p.leadingCoeff) : (p.map f).leadingCoeff = f p.leadingCoeff :=
+  leadingCoeff_map_of_leadingCoeff_ne_zero _ <| f.isUnit_map hp |>.ne_zero
+
+theorem nextCoeff_map_eq_of_isUnit_leadingCoeff [Nontrivial S] (f : R →+* S)
+    (hp : IsUnit p.leadingCoeff) : (p.map f).nextCoeff = f p.nextCoeff :=
+  nextCoeff_map_of_leadingCoeff_ne_zero _ <| f.isUnit_map hp |>.ne_zero
+
+theorem degree_map_eq_of_injective {f : R →+* S} (hf : Function.Injective f) (p : Polynomial R) :
+    (p.map f).degree = p.degree := by
+  simp [hf, map_ne_zero_iff, ne_or_eq]
+
+theorem natDegree_map_eq_of_injective {f : R →+* S} (hf : Function.Injective f) (p : Polynomial R) :
+    (p.map f).natDegree = p.natDegree :=
+  natDegree_eq_of_degree_eq <| degree_map_eq_of_injective hf _
+
+theorem leadingCoeff_map_of_injective {f : R →+* S} (hf : Function.Injective f)
+    (p : Polynomial R) : (p.map f).leadingCoeff = f p.leadingCoeff := by
+  simp only [leadingCoeff, natDegree_map_eq_of_injective hf, coeff_map]
+
+theorem nextCoeff_map {f : R →+* S} (hf : Function.Injective f) (p : Polynomial R) :
+    (p.map f).nextCoeff = f p.nextCoeff := by
+  simp only [hf, nextCoeff, natDegree_map_eq_of_injective]
+  split_ifs <;> simp
+
 theorem natDegree_pos_of_nextCoeff_ne_zero (h : p.nextCoeff ≠ 0) : 0 < p.natDegree := by
   grind [nextCoeff]
 
@@ -323,6 +356,13 @@ lemma natDegree_eq_one : p.natDegree = 1 ↔ ∃ a ≠ 0, ∃ b, C a * X + C b =
   · rintro ⟨a, ha, b, rfl⟩
     simp [ha]
 
+theorem subsingleton_isRoot_of_natDegree_eq_one [IsLeftCancelMulZero R] [IsRightCancelAdd R]
+    (h : p.natDegree = 1) : { x | IsRoot p x }.Subsingleton := by
+  intro r₁
+  obtain ⟨r₂, hr₂, r₃, rfl⟩ : ∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = p := by rwa [natDegree_eq_one] at h
+  have (x y : R) := mul_left_cancel₀ hr₂ (b := x) (c := y)
+  grind [IsRoot, eval_add, eval_mul_X, eval_C]
+
 variable [NoZeroDivisors R]
 
 theorem degree_mul_C (a0 : a ≠ 0) : (p * C a).degree = p.degree := by
@@ -357,6 +397,14 @@ theorem leadingCoeff_comp (hq : natDegree q ≠ 0) :
     leadingCoeff (p.comp q) = leadingCoeff p * leadingCoeff q ^ natDegree p := by
   rw [← coeff_comp_degree_mul_degree hq, ← natDegree_comp, coeff_natDegree]
 
+@[simp]
+theorem nextCoeff_C_mul : (C a * p).nextCoeff = a * p.nextCoeff := by
+  by_cases h₀ : a = 0 <;> simp [h₀, nextCoeff, natDegree_C_mul]
+
+@[simp]
+theorem nextCoeff_mul_C : (p * C a).nextCoeff = p.nextCoeff * a := by
+  by_cases h₀ : a = 0 <;> simp [h₀, nextCoeff, natDegree_mul_C]
+
 end NoZeroDivisors
 
 @[simp] lemma comp_neg_X_leadingCoeff_eq [Ring R] (p : R[X]) :

Mathlib/Algebra/Polynomial/Div.lean

@@ -704,6 +704,11 @@ lemma le_rootMultiplicity_mul {p q : R[X]} (x : R) (hpq : p * q ≠ 0) :
   rw [le_rootMultiplicity_iff hpq, pow_add]
   gcongr <;> apply pow_rootMultiplicity_dvd
 
+lemma rootMultiplicity_le_rootMultiplicity_of_dvd {p q : R[X]} (hq : q ≠ 0) (hpq : p ∣ q) (x : R) :
+    p.rootMultiplicity x ≤ q.rootMultiplicity x := by
+  obtain ⟨_, rfl⟩ := hpq
+  exact Nat.le_of_add_right_le <| le_rootMultiplicity_mul x hq
+
 lemma pow_rootMultiplicity_not_dvd (p0 : p ≠ 0) (a : R) :
     ¬(X - C a) ^ (rootMultiplicity a p + 1) ∣ p := by rw [← rootMultiplicity_le_iff p0]
 
@@ -743,6 +748,19 @@ lemma degree_eq_one_of_irreducible_of_root (hi : Irreducible p) {x : R} (hx : Is
       rw [h₁] at h₂; exact absurd h₂ (by decide))
     fun hgu => by rw [hg, degree_mul, degree_X_sub_C, degree_eq_zero_of_isUnit hgu, add_zero]
 
+lemma _root_.Irreducible.not_isRoot_of_natDegree_ne_one
+    (hi : Irreducible p) (hdeg : p.natDegree ≠ 1) {x : R} : ¬p.IsRoot x :=
+  fun hr ↦ hdeg <| natDegree_eq_of_degree_eq_some <| degree_eq_one_of_irreducible_of_root hi hr
+
+lemma _root_.Irreducible.isRoot_eq_bot_of_natDegree_ne_one
+    (hi : Irreducible p) (hdeg : p.natDegree ≠ 1) : p.IsRoot = ⊥ :=
+  le_bot_iff.mp fun _ ↦ hi.not_isRoot_of_natDegree_ne_one hdeg
+
+lemma _root_.Irreducible.subsingleton_isRoot [IsLeftCancelMulZero R] [IsRightCancelAdd R]
+    (hi : Irreducible p) : { x | p.IsRoot x }.Subsingleton :=
+  fun _ hx ↦ (subsingleton_isRoot_of_natDegree_eq_one <| natDegree_eq_of_degree_eq_some <|
+    degree_eq_one_of_irreducible_of_root hi hx) hx
+
 lemma leadingCoeff_divByMonic_X_sub_C (p : R[X]) (hp : degree p ≠ 0) (a : R) :
     leadingCoeff (p /ₘ (X - C a)) = leadingCoeff p := by
   nontriviality

Mathlib/Algebra/Polynomial/Eval/Coeff.lean

@@ -58,8 +58,11 @@ theorem coeff_zero_eq_eval_zero (p : R[X]) : coeff p 0 = p.eval 0 :=
       rw [eval_eq_sum]
       exact Finset.sum_eq_single _ (fun b _ hb => by simp [zero_pow hb]) (by simp)
 
-theorem zero_isRoot_of_coeff_zero_eq_zero {p : R[X]} (hp : p.coeff 0 = 0) : IsRoot p 0 := by
-  rwa [coeff_zero_eq_eval_zero] at hp
+theorem zero_isRoot_iff_coeff_zero_eq_zero {p : R[X]} : IsRoot p 0 ↔ p.coeff 0 = 0 := by
+  rw [coeff_zero_eq_eval_zero, IsRoot]
+
+alias ⟨coeff_zero_eq_zero_of_zero_isRoot, zero_isRoot_of_coeff_zero_eq_zero⟩ :=
+  zero_isRoot_iff_coeff_zero_eq_zero
 
 end Eval
 

Mathlib/Algebra/Polynomial/Eval/Defs.lean

@@ -552,6 +552,9 @@ protected theorem map_pow (n : ℕ) : (p ^ n).map f = p.map f ^ n :=
 theorem eval_map (x : S) : (p.map f).eval x = p.eval₂ f x :=
   (eval₂_eq_eval_map f).symm
 
+@[simp] lemma eval_map_apply (x : R) : (p.map f).eval (f x) = f (p.eval x) :=
+  eval_map f _ ▸ eval₂_at_apply ..
+
 protected theorem map_sum {ι : Type*} (g : ι → R[X]) (s : Finset ι) :
     (∑ i ∈ s, g i).map f = ∑ i ∈ s, (g i).map f :=
   map_sum (mapRingHom f) _ _

Mathlib/Algebra/Polynomial/Eval/Degree.lean

@@ -182,6 +182,10 @@ theorem leadingCoeff_map_of_leadingCoeff_ne_zero (f : R →+* S) (hf : f (leadin
   unfold leadingCoeff
   rw [coeff_map, natDegree_map_of_leadingCoeff_ne_zero f hf]
 
+theorem nextCoeff_map_of_leadingCoeff_ne_zero (f : R →+* S) (hf : f p.leadingCoeff ≠ 0) :
+    (p.map f).nextCoeff = f p.nextCoeff := by
+  grind [nextCoeff, natDegree_map_of_leadingCoeff_ne_zero, coeff_map, map_zero]
+
 end Map
 
 end Semiring

Mathlib/Algebra/Polynomial/FieldDivision.lean

@@ -249,35 +249,38 @@ theorem degree_pos_of_ne_zero_of_nonunit (hp0 : p ≠ 0) (hp : ¬IsUnit p) : 0 <
     rw [eq_C_of_degree_le_zero h] at hp0 hp
     exact hp (IsUnit.map C (IsUnit.mk0 (coeff p 0) (mt C_inj.2 (by simpa using hp0))))
 
+end DivisionRing
+
+section SimpleRing
+
+variable [Ring R] [IsSimpleRing R] [Semiring S] [Nontrivial S] {p q : R[X]}
+
 @[simp]
-protected theorem map_eq_zero [Semiring S] [Nontrivial S] (f : R →+* S) : p.map f = 0 ↔ p = 0 := by
-  simp only [Polynomial.ext_iff]
-  congr!
-  simp [map_eq_zero, coeff_map, coeff_zero]
+protected theorem map_eq_zero (f : R →+* S) : p.map f = 0 ↔ p = 0 :=
+  Polynomial.map_eq_zero_iff f.injective
 
-theorem map_ne_zero [Semiring S] [Nontrivial S] {f : R →+* S} (hp : p ≠ 0) : p.map f ≠ 0 :=
+theorem map_ne_zero {f : R →+* S} (hp : p ≠ 0) : p.map f ≠ 0 :=
   mt (Polynomial.map_eq_zero f).1 hp
 
 @[simp]
-theorem degree_map [Semiring S] [Nontrivial S] (p : R[X]) (f : R →+* S) :
-    degree (p.map f) = degree p :=
-  p.degree_map_eq_of_injective f.injective
+theorem degree_map (p : R[X]) (f : R →+* S) : (p.map f).degree = p.degree :=
+  degree_map_eq_of_injective f.injective _
 
 @[simp]
-theorem natDegree_map [Semiring S] [Nontrivial S] (f : R →+* S) :
-    natDegree (p.map f) = natDegree p :=
-  natDegree_eq_of_degree_eq (degree_map _ f)
+theorem natDegree_map (f : R →+* S) : (p.map f).natDegree = p.natDegree :=
+  natDegree_map_eq_of_injective f.injective _
 
 @[simp]
-theorem leadingCoeff_map [Semiring S] [Nontrivial S] (f : R →+* S) :
-    leadingCoeff (p.map f) = f (leadingCoeff p) := by
-  simp only [← coeff_natDegree, coeff_map f, natDegree_map]
+theorem leadingCoeff_map (f : R →+* S) : (p.map f).leadingCoeff = f p.leadingCoeff :=
+  leadingCoeff_map_of_injective f.injective _
 
-theorem monic_map_iff [Semiring S] [Nontrivial S] {f : R →+* S} {p : R[X]} :
-    (p.map f).Monic ↔ p.Monic := by
-  rw [Monic, leadingCoeff_map, ← f.map_one, Function.Injective.eq_iff f.injective, Monic]
+theorem nextCoeff_map_eq (p : R[X]) (f : R →+* S) : (p.map f).nextCoeff = f p.nextCoeff :=
+  nextCoeff_map f.injective _
 
-end DivisionRing
+@[simp] theorem monic_map_iff {f : R →+* S} {p : R[X]} : (p.map f).Monic ↔ p.Monic :=
+  Function.Injective.monic_map_iff f.injective |>.symm
+
+end SimpleRing
 
 section Field
 

Mathlib/Algebra/Polynomial/Monic.lean

@@ -52,15 +52,9 @@ theorem Monic.as_sum (hp : p.Monic) :
 @[deprecated (since := "2025-08-14")] alias ne_zero_of_ne_zero_of_monic :=
   Monic.ne_zero_of_polynomial_ne
 
-theorem Monic.map [Semiring S] (f : R →+* S) (hp : Monic p) : Monic (p.map f) := by
-  unfold Monic
-  nontriviality
-  have : f p.leadingCoeff ≠ 0 := by
-    rw [show _ = _ from hp, f.map_one]
-    exact one_ne_zero
-  rw [Polynomial.leadingCoeff, coeff_map]
-  suffices p.coeff (p.map f).natDegree = 1 by simp [this]
-  rwa [natDegree_eq_of_degree_eq (degree_map_eq_of_leadingCoeff_ne_zero f this)]
+theorem Monic.map [Semiring S] (f : R →+* S) (hp : Monic p) : Monic (p.map f) :=
+  subsingleton_or_nontrivial S |>.elim (·.elim ..) fun _ ↦
+    f.map_one ▸ hp ▸ leadingCoeff_map_eq_of_isUnit_leadingCoeff _ <| hp ▸ isUnit_one
 
 theorem monic_C_mul_of_mul_leadingCoeff_eq_one {b : R} (hp : b * p.leadingCoeff = 1) :
     Monic (C b * p) := by
@@ -366,32 +360,11 @@ open Function
 
 variable [Semiring S] {f : R →+* S}
 
-theorem degree_map_eq_of_injective (hf : Injective f) (p : R[X]) : degree (p.map f) = degree p :=
-  letI := Classical.decEq R
-  if h : p = 0 then by simp [h]
-  else
-    degree_map_eq_of_leadingCoeff_ne_zero _
-      (by rw [← f.map_zero]; exact mt hf.eq_iff.1 (mt leadingCoeff_eq_zero.1 h))
-
-theorem natDegree_map_eq_of_injective (hf : Injective f) (p : R[X]) :
-    natDegree (p.map f) = natDegree p :=
-  natDegree_eq_of_degree_eq (degree_map_eq_of_injective hf p)
-
-theorem leadingCoeff_map_of_injective (hf : Injective f) (p : R[X]) :
-    leadingCoeff (p.map f) = f (leadingCoeff p) := by
-  unfold leadingCoeff
-  rw [coeff_map, natDegree_map_eq_of_injective hf p]
-
 @[deprecated (since := "2025-10-26")]
 alias leadingCoeff_map' := leadingCoeff_map_of_injective
 @[deprecated (since := "2025-10-26")]
 alias leadingCoeff_of_injective := leadingCoeff_map_of_injective
 
-theorem nextCoeff_map (hf : Injective f) (p : R[X]) : (p.map f).nextCoeff = f p.nextCoeff := by
-  unfold nextCoeff
-  rw [natDegree_map_eq_of_injective hf]
-  split_ifs <;> simp [*]
-
 theorem monic_of_injective (hf : Injective f) {p : R[X]} (hp : (p.map f).Monic) : p.Monic := by
   apply hf
   rw [← leadingCoeff_map_of_injective hf, hp.leadingCoeff, f.map_one]

Mathlib/Algebra/Polynomial/RingDivision.lean

@@ -130,6 +130,14 @@ theorem mem_nonZeroDivisors_of_trailingCoeff {p : R[X]} (h : p.trailingCoeff ∈
 
 end nonZeroDivisors
 
+lemma _root_.Irreducible.aeval_ne_zero_of_natDegree_ne_one [IsDomain R] [Ring S] [Algebra R S]
+    [FaithfulSMul R S] {p : R[X]} (hp : Irreducible p) (hdeg : p.natDegree ≠ 1) {x : S}
+    (hx : x ∈ (algebraMap R S).range) : p.aeval x ≠ 0 := by
+  obtain ⟨_, rfl⟩ := hx
+  rw [aeval_algebraMap_apply_eq_algebraMap_eval]
+  exact fun heq ↦ hp.not_isRoot_of_natDegree_ne_one hdeg <|
+    FaithfulSMul.algebraMap_injective _ _ <| map_zero (algebraMap R S) ▸ heq
+
 theorem natDegree_pos_of_monic_of_aeval_eq_zero [Nontrivial R] [Semiring S] [Algebra R S]
     [FaithfulSMul R S] {p : R[X]} (hp : p.Monic) {x : S} (hx : aeval x p = 0) :
     0 < p.natDegree :=