chore(Algebra/Polynomial/RingDivision): move lemmas earlier (#18050)

`Algebra.Polynomial.RingDivision` is a bag grab of lemmas with absolutely no running theme. This PR moves two thirds of them to earlier files with no proof change.

Author: YaelDillies

Mathlib/Algebra/Polynomial/AlgebraMap.lean

@@ -531,11 +531,30 @@ theorem not_isUnit_X_sub_C [Nontrivial R] (r : R) : ¬IsUnit (X - C r) :=
 
 end Ring
 
-theorem aeval_endomorphism {M : Type*} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M)
+section CommRing
+variable [CommRing R] {p : R[X]} {t : R}
+
+theorem aeval_endomorphism {M : Type*} [AddCommGroup M] [Module R M] (f : M →ₗ[R] M)
     (v : M) (p : R[X]) : aeval f p v = p.sum fun n b => b • (f ^ n) v := by
   rw [aeval_def, eval₂_eq_sum]
   exact map_sum (LinearMap.applyₗ v) _ _
 
+lemma X_sub_C_pow_dvd_iff {n : ℕ} : (X - C t) ^ n ∣ p ↔ X ^ n ∣ p.comp (X + C t) := by
+  convert (map_dvd_iff <| algEquivAevalXAddC t).symm using 2
+  simp [C_eq_algebraMap]
+
+lemma comp_X_add_C_eq_zero_iff : p.comp (X + C t) = 0 ↔ p = 0 :=
+  AddEquivClass.map_eq_zero_iff (algEquivAevalXAddC t)
+
+lemma comp_X_add_C_ne_zero_iff : p.comp (X + C t) ≠ 0 ↔ p ≠ 0 := comp_X_add_C_eq_zero_iff.not
+
+variable [IsDomain R]
+
+lemma units_coeff_zero_smul (c : R[X]ˣ) (p : R[X]) : (c : R[X]).coeff 0 • p = c * p := by
+  rw [← Polynomial.C_mul', ← Polynomial.eq_C_of_degree_eq_zero (degree_coe_units c)]
+
+end CommRing
+
 section StableSubmodule
 
 variable {M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M]
@@ -561,4 +580,55 @@ lemma aeval_apply_smul_mem_of_le_comap
 
 end StableSubmodule
 
+section CommSemiring
+
+variable [CommSemiring R] {a p : R[X]}
+
+theorem eq_zero_of_mul_eq_zero_of_smul (P : R[X]) (h : ∀ r : R, r • P = 0 → r = 0) :
+    ∀ (Q : R[X]), P * Q = 0 → Q = 0 := by
+  intro Q hQ
+  suffices ∀ i, P.coeff i • Q = 0 by
+    rw [← leadingCoeff_eq_zero]
+    apply h
+    simpa [ext_iff, mul_comm Q.leadingCoeff] using fun i ↦ congr_arg (·.coeff Q.natDegree) (this i)
+  apply Nat.strong_decreasing_induction
+  · use P.natDegree
+    intro i hi
+    rw [coeff_eq_zero_of_natDegree_lt hi, zero_smul]
+  intro l IH
+  obtain _|hl := (natDegree_smul_le (P.coeff l) Q).lt_or_eq
+  · apply eq_zero_of_mul_eq_zero_of_smul _ h (P.coeff l • Q)
+    rw [smul_eq_C_mul, mul_left_comm, hQ, mul_zero]
+  suffices P.coeff l * Q.leadingCoeff = 0 by
+    rwa [← leadingCoeff_eq_zero, ← coeff_natDegree, coeff_smul, hl, coeff_natDegree, smul_eq_mul]
+  let m := Q.natDegree
+  suffices (P * Q).coeff (l + m) = P.coeff l * Q.leadingCoeff by rw [← this, hQ, coeff_zero]
+  rw [coeff_mul]
+  apply Finset.sum_eq_single (l, m) _ (by simp)
+  simp only [Finset.mem_antidiagonal, ne_eq, Prod.forall, Prod.mk.injEq, not_and]
+  intro i j hij H
+  obtain hi|rfl|hi := lt_trichotomy i l
+  · have hj : m < j := by omega
+    rw [coeff_eq_zero_of_natDegree_lt hj, mul_zero]
+  · omega
+  · rw [← coeff_C_mul, ← smul_eq_C_mul, IH _ hi, coeff_zero]
+termination_by Q => Q.natDegree
+
+open nonZeroDivisors in
+/-- *McCoy theorem*: a polynomial `P : R[X]` is a zerodivisor if and only if there is `a : R`
+such that `a ≠ 0` and `a • P = 0`. -/
+theorem nmem_nonZeroDivisors_iff {P : R[X]} : P ∉ R[X]⁰ ↔ ∃ a : R, a ≠ 0 ∧ a • P = 0 := by
+  refine ⟨fun hP ↦ ?_, fun ⟨a, ha, h⟩ h1 ↦ ha <| C_eq_zero.1 <| (h1 _) <| smul_eq_C_mul a ▸ h⟩
+  by_contra! h
+  obtain ⟨Q, hQ⟩ := _root_.nmem_nonZeroDivisors_iff.1 hP
+  refine hQ.2 (eq_zero_of_mul_eq_zero_of_smul P (fun a ha ↦ ?_) Q (mul_comm P _ ▸ hQ.1))
+  contrapose! ha
+  exact h a ha
+
+open nonZeroDivisors in
+protected lemma mem_nonZeroDivisors_iff {P : R[X]} : P ∈ R[X]⁰ ↔ ∀ a : R, a • P = 0 → a = 0 := by
+  simpa [not_imp_not] using (nmem_nonZeroDivisors_iff (P := P)).not
+
+end CommSemiring
+
 end Polynomial

Mathlib/Algebra/Polynomial/BigOperators.lean

@@ -270,6 +270,16 @@ theorem prod_X_sub_C_coeff_card_pred (s : Finset ι) (f : ι → R) (hs : 0 < #s
     (∏ i ∈ s, (X - C (f i))).coeff (#s - 1) = -∑ i ∈ s, f i := by
   simpa using multiset_prod_X_sub_C_coeff_card_pred (s.1.map f) (by simpa using hs)
 
+variable [IsDomain R]
+
+@[simp]
+lemma natDegree_multiset_prod_X_sub_C_eq_card (s : Multiset R) :
+    (s.map (X - C ·)).prod.natDegree = Multiset.card s := by
+  rw [natDegree_multiset_prod_of_monic, Multiset.map_map]
+  · simp only [(· ∘ ·), natDegree_X_sub_C, Multiset.map_const', Multiset.sum_replicate, smul_eq_mul,
+      mul_one]
+  · exact Multiset.forall_mem_map_iff.2 fun a _ => monic_X_sub_C a
+
 end CommRing
 
 section NoZeroDivisors

Mathlib/Algebra/Polynomial/Degree/Definitions.lean

@@ -1370,8 +1370,188 @@ theorem leadingCoeff_pow_X_add_C (r : R) (i : ℕ) : leadingCoeff ((X + C r) ^ i
   nontriviality
   rw [leadingCoeff_pow'] <;> simp
 
+variable [NoZeroDivisors R] {p q : R[X]}
+
+@[simp]
+lemma degree_mul : degree (p * q) = degree p + degree q :=
+  letI := Classical.decEq R
+  if hp0 : p = 0 then by simp only [hp0, degree_zero, zero_mul, WithBot.bot_add]
+  else
+    if hq0 : q = 0 then by simp only [hq0, degree_zero, mul_zero, WithBot.add_bot]
+    else degree_mul' <| mul_ne_zero (mt leadingCoeff_eq_zero.1 hp0) (mt leadingCoeff_eq_zero.1 hq0)
+
+/-- `degree` as a monoid homomorphism between `R[X]` and `Multiplicative (WithBot ℕ)`.
+  This is useful to prove results about multiplication and degree. -/
+def degreeMonoidHom [Nontrivial R] : R[X] →* Multiplicative (WithBot ℕ) where
+  toFun := degree
+  map_one' := degree_one
+  map_mul' _ _ := degree_mul
+
+@[simp]
+lemma degree_pow [Nontrivial R] (p : R[X]) (n : ℕ) : degree (p ^ n) = n • degree p :=
+  map_pow (@degreeMonoidHom R _ _ _) _ _
+
+@[simp]
+lemma leadingCoeff_mul (p q : R[X]) : leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q := by
+  by_cases hp : p = 0
+  · simp only [hp, zero_mul, leadingCoeff_zero]
+  · by_cases hq : q = 0
+    · simp only [hq, mul_zero, leadingCoeff_zero]
+    · rw [leadingCoeff_mul']
+      exact mul_ne_zero (mt leadingCoeff_eq_zero.1 hp) (mt leadingCoeff_eq_zero.1 hq)
+
+/-- `Polynomial.leadingCoeff` bundled as a `MonoidHom` when `R` has `NoZeroDivisors`, and thus
+  `leadingCoeff` is multiplicative -/
+def leadingCoeffHom : R[X] →* R where
+  toFun := leadingCoeff
+  map_one' := by simp
+  map_mul' := leadingCoeff_mul
+
+@[simp]
+lemma leadingCoeffHom_apply (p : R[X]) : leadingCoeffHom p = leadingCoeff p :=
+  rfl
+
+@[simp]
+lemma leadingCoeff_pow (p : R[X]) (n : ℕ) : leadingCoeff (p ^ n) = leadingCoeff p ^ n :=
+  (leadingCoeffHom : R[X] →* R).map_pow p n
+
+lemma leadingCoeff_dvd_leadingCoeff {a p : R[X]} (hap : a ∣ p) :
+    a.leadingCoeff ∣ p.leadingCoeff :=
+  map_dvd leadingCoeffHom hap
+
+instance : NoZeroDivisors R[X] where
+  eq_zero_or_eq_zero_of_mul_eq_zero h := by
+    rw [← leadingCoeff_eq_zero, ← leadingCoeff_eq_zero]
+    refine eq_zero_or_eq_zero_of_mul_eq_zero ?_
+    rw [← leadingCoeff_zero, ← leadingCoeff_mul, h]
+lemma natDegree_mul (hp : p ≠ 0) (hq : q ≠ 0) : (p*q).natDegree = p.natDegree + q.natDegree := by
+  rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree (mul_ne_zero hp hq),
+    Nat.cast_add, ← degree_eq_natDegree hp, ← degree_eq_natDegree hq, degree_mul]
+
+@[simp]
+lemma natDegree_pow (p : R[X]) (n : ℕ) : natDegree (p ^ n) = n * natDegree p := by
+  classical
+  obtain rfl | hp := eq_or_ne p 0
+  · obtain rfl | hn := eq_or_ne n 0 <;> simp [*]
+  exact natDegree_pow' <| by
+    rw [← leadingCoeff_pow, Ne, leadingCoeff_eq_zero]; exact pow_ne_zero _ hp
+
+lemma degree_le_mul_left (p : R[X]) (hq : q ≠ 0) : degree p ≤ degree (p * q) := by
+  classical
+  obtain rfl | hp := eq_or_ne p 0
+  · simp
+  · rw [degree_mul, degree_eq_natDegree hp, degree_eq_natDegree hq]
+    exact WithBot.coe_le_coe.2 (Nat.le_add_right _ _)
+
+lemma natDegree_le_of_dvd (h1 : p ∣ q) (h2 : q ≠ 0) : p.natDegree ≤ q.natDegree := by
+  obtain ⟨q, rfl⟩ := h1
+  rw [mul_ne_zero_iff] at h2
+  rw [natDegree_mul h2.1 h2.2]; exact Nat.le_add_right _ _
+
+lemma degree_le_of_dvd (h1 : p ∣ q) (h2 : q ≠ 0) : degree p ≤ degree q := by
+  rcases h1 with ⟨q, rfl⟩; rw [mul_ne_zero_iff] at h2
+  exact degree_le_mul_left p h2.2
+
+lemma eq_zero_of_dvd_of_degree_lt (h₁ : p ∣ q) (h₂ : degree q < degree p) : q = 0 := by
+  by_contra hc
+  exact (lt_iff_not_ge _ _).mp h₂ (degree_le_of_dvd h₁ hc)
+
+lemma eq_zero_of_dvd_of_natDegree_lt (h₁ : p ∣ q) (h₂ : natDegree q < natDegree p) :
+    q = 0 := by
+  by_contra hc
+  exact (lt_iff_not_ge _ _).mp h₂ (natDegree_le_of_dvd h₁ hc)
+
+lemma not_dvd_of_degree_lt (h0 : q ≠ 0) (hl : q.degree < p.degree) : ¬p ∣ q := by
+  by_contra hcontra
+  exact h0 (eq_zero_of_dvd_of_degree_lt hcontra hl)
+
+lemma not_dvd_of_natDegree_lt (h0 : q ≠ 0) (hl : q.natDegree < p.natDegree) :
+    ¬p ∣ q := by
+  by_contra hcontra
+  exact h0 (eq_zero_of_dvd_of_natDegree_lt hcontra hl)
+
+/-- This lemma is useful for working with the `intDegree` of a rational function. -/
+lemma natDegree_sub_eq_of_prod_eq {p₁ p₂ q₁ q₂ : R[X]} (hp₁ : p₁ ≠ 0) (hq₁ : q₁ ≠ 0)
+    (hp₂ : p₂ ≠ 0) (hq₂ : q₂ ≠ 0) (h_eq : p₁ * q₂ = p₂ * q₁) :
+    (p₁.natDegree : ℤ) - q₁.natDegree = (p₂.natDegree : ℤ) - q₂.natDegree := by
+  rw [sub_eq_sub_iff_add_eq_add]
+  norm_cast
+  rw [← natDegree_mul hp₁ hq₂, ← natDegree_mul hp₂ hq₁, h_eq]
+
+lemma natDegree_eq_zero_of_isUnit (h : IsUnit p) : natDegree p = 0 := by
+  nontriviality R
+  obtain ⟨q, hq⟩ := h.exists_right_inv
+  have := natDegree_mul (left_ne_zero_of_mul_eq_one hq) (right_ne_zero_of_mul_eq_one hq)
+  rw [hq, natDegree_one, eq_comm, add_eq_zero] at this
+  exact this.1
+
+lemma degree_eq_zero_of_isUnit [Nontrivial R] (h : IsUnit p) : degree p = 0 :=
+  (natDegree_eq_zero_iff_degree_le_zero.mp <| natDegree_eq_zero_of_isUnit h).antisymm
+    (zero_le_degree_iff.mpr h.ne_zero)
+
+@[simp]
+lemma degree_coe_units [Nontrivial R] (u : R[X]ˣ) : degree (u : R[X]) = 0 :=
+  degree_eq_zero_of_isUnit ⟨u, rfl⟩
+
+/-- Characterization of a unit of a polynomial ring over an integral domain `R`.
+See `Polynomial.isUnit_iff_coeff_isUnit_isNilpotent` when `R` is a commutative ring. -/
+lemma isUnit_iff : IsUnit p ↔ ∃ r : R, IsUnit r ∧ C r = p :=
+  ⟨fun hp =>
+    ⟨p.coeff 0,
+      let h := eq_C_of_natDegree_eq_zero (natDegree_eq_zero_of_isUnit hp)
+      ⟨isUnit_C.1 (h ▸ hp), h.symm⟩⟩,
+    fun ⟨_, hr, hrp⟩ => hrp ▸ isUnit_C.2 hr⟩
+
+lemma not_isUnit_of_degree_pos (p : R[X]) (hpl : 0 < p.degree) : ¬ IsUnit p := by
+  cases subsingleton_or_nontrivial R
+  · simp [Subsingleton.elim p 0] at hpl
+  intro h
+  simp [degree_eq_zero_of_isUnit h] at hpl
+
+lemma not_isUnit_of_natDegree_pos (p : R[X]) (hpl : 0 < p.natDegree) : ¬ IsUnit p :=
+  not_isUnit_of_degree_pos _ (natDegree_pos_iff_degree_pos.mp hpl)
+
+@[simp] lemma natDegree_coe_units (u : R[X]ˣ) : natDegree (u : R[X]) = 0 := by
+  nontriviality R
+  exact natDegree_eq_of_degree_eq_some (degree_coe_units u)
+
+theorem coeff_coe_units_zero_ne_zero [Nontrivial R] (u : R[X]ˣ) : coeff (u : R[X]) 0 ≠ 0 := by
+  conv in 0 => rw [← natDegree_coe_units u]
+  rw [← leadingCoeff, Ne, leadingCoeff_eq_zero]
+  exact Units.ne_zero _
+
 end Semiring
 
+section CommSemiring
+variable [CommSemiring R] {a p : R[X]} (hp : p.Monic)
+include hp
+
+lemma Monic.C_dvd_iff_isUnit {a : R} : C a ∣ p ↔ IsUnit a where
+  mp h := isUnit_iff_dvd_one.mpr <| hp.coeff_natDegree ▸ (C_dvd_iff_dvd_coeff _ _).mp h p.natDegree
+  mpr ha := (ha.map C).dvd
+
+lemma Monic.natDegree_pos : 0 < natDegree p ↔ p ≠ 1 :=
+  Nat.pos_iff_ne_zero.trans hp.natDegree_eq_zero.not
+
+lemma Monic.degree_pos : 0 < degree p ↔ p ≠ 1 :=
+  natDegree_pos_iff_degree_pos.symm.trans hp.natDegree_pos
+
+lemma Monic.degree_pos_of_not_isUnit (hu : ¬IsUnit p) : 0 < degree p :=
+  hp.degree_pos.mpr fun hp' ↦ (hp' ▸ hu) isUnit_one
+
+lemma Monic.natDegree_pos_of_not_isUnit (hu : ¬IsUnit p) : 0 < natDegree p :=
+  hp.natDegree_pos.mpr fun hp' ↦ (hp' ▸ hu) isUnit_one
+
+lemma degree_pos_of_not_isUnit_of_dvd_monic (ha : ¬IsUnit a) (hap : a ∣ p) : 0 < degree a := by
+  contrapose! ha with h
+  rw [Polynomial.eq_C_of_degree_le_zero h] at hap ⊢
+  simpa [hp.C_dvd_iff_isUnit, isUnit_C] using hap
+
+lemma natDegree_pos_of_not_isUnit_of_dvd_monic (ha : ¬IsUnit a) (hap : a ∣ p) : 0 < natDegree a :=
+  natDegree_pos_iff_degree_pos.mpr <| degree_pos_of_not_isUnit_of_dvd_monic hp ha hap
+
+end CommSemiring
+
 section Ring
 
 variable [Ring R]
@@ -1420,59 +1600,11 @@ theorem natDegree_X_pow_sub_C {n : ℕ} {r : R} : (X ^ n - C r).natDegree = n :=
 theorem leadingCoeff_X_sub_C [Ring S] (r : S) : (X - C r).leadingCoeff = 1 := by
   rw [sub_eq_add_neg, ← map_neg C r, leadingCoeff_X_add_C]
 
-end Ring
-
-section NoZeroDivisors
-
-variable [Semiring R] [NoZeroDivisors R] {p q : R[X]}
-
-@[simp]
-theorem degree_mul : degree (p * q) = degree p + degree q :=
-  letI := Classical.decEq R
-  if hp0 : p = 0 then by simp only [hp0, degree_zero, zero_mul, WithBot.bot_add]
-  else
-    if hq0 : q = 0 then by simp only [hq0, degree_zero, mul_zero, WithBot.add_bot]
-    else degree_mul' <| mul_ne_zero (mt leadingCoeff_eq_zero.1 hp0) (mt leadingCoeff_eq_zero.1 hq0)
-
-/-- `degree` as a monoid homomorphism between `R[X]` and `Multiplicative (WithBot ℕ)`.
-  This is useful to prove results about multiplication and degree. -/
-def degreeMonoidHom [Nontrivial R] : R[X] →* Multiplicative (WithBot ℕ) where
-  toFun := degree
-  map_one' := degree_one
-  map_mul' _ _ := degree_mul
+variable [IsDomain R] {p q : R[X]}
 
-@[simp]
-theorem degree_pow [Nontrivial R] (p : R[X]) (n : ℕ) : degree (p ^ n) = n • degree p :=
-  map_pow (@degreeMonoidHom R _ _ _) _ _
-
-@[simp]
-theorem leadingCoeff_mul (p q : R[X]) : leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q := by
-  by_cases hp : p = 0
-  · simp only [hp, zero_mul, leadingCoeff_zero]
-  · by_cases hq : q = 0
-    · simp only [hq, mul_zero, leadingCoeff_zero]
-    · rw [leadingCoeff_mul']
-      exact mul_ne_zero (mt leadingCoeff_eq_zero.1 hp) (mt leadingCoeff_eq_zero.1 hq)
-
-/-- `Polynomial.leadingCoeff` bundled as a `MonoidHom` when `R` has `NoZeroDivisors`, and thus
-  `leadingCoeff` is multiplicative -/
-def leadingCoeffHom : R[X] →* R where
-  toFun := leadingCoeff
-  map_one' := by simp
-  map_mul' := leadingCoeff_mul
-
-@[simp]
-theorem leadingCoeffHom_apply (p : R[X]) : leadingCoeffHom p = leadingCoeff p :=
-  rfl
-
-@[simp]
-theorem leadingCoeff_pow (p : R[X]) (n : ℕ) : leadingCoeff (p ^ n) = leadingCoeff p ^ n :=
-  (leadingCoeffHom : R[X] →* R).map_pow p n
-
-theorem leadingCoeff_dvd_leadingCoeff {a p : R[X]} (hap : a ∣ p) :
-    a.leadingCoeff ∣ p.leadingCoeff :=
-  map_dvd leadingCoeffHom hap
-
-end NoZeroDivisors
+instance : IsDomain R[X] := NoZeroDivisors.to_isDomain _
 
+end Ring
 end Polynomial
+
+set_option linter.style.longFile 1700

Mathlib/Algebra/Polynomial/Degree/Lemmas.lean

@@ -368,6 +368,31 @@ 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]) :
+    (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]
+
+lemma comp_eq_zero_iff : 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]
+  obtain key | key := Or.imp eq_C_of_natDegree_eq_zero eq_C_of_natDegree_eq_zero key
+  · rw [key, C_comp] at h
+    exact Or.inl (key.trans h)
+  · rw [key, comp_C, C_eq_zero] at h
+    exact Or.inr ⟨h, key⟩
+
+end CommRing
+
 section DivisionRing
 
 variable {K : Type*} [DivisionRing K]