feat: lemmas about nilpotency and polynomials (#6450)

Author: ocfnash

Mathlib.lean

@@ -2034,6 +2034,7 @@ import Mathlib.GroupTheory.Submonoid.Inverses
 import Mathlib.GroupTheory.Submonoid.Membership
 import Mathlib.GroupTheory.Submonoid.Operations
 import Mathlib.GroupTheory.Submonoid.Pointwise
+import Mathlib.GroupTheory.Submonoid.ZeroDivisors
 import Mathlib.GroupTheory.Subsemigroup.Basic
 import Mathlib.GroupTheory.Subsemigroup.Center
 import Mathlib.GroupTheory.Subsemigroup.Centralizer
@@ -2842,6 +2843,7 @@ import Mathlib.RingTheory.Polynomial.GaussLemma
 import Mathlib.RingTheory.Polynomial.Hermite.Basic
 import Mathlib.RingTheory.Polynomial.Hermite.Gaussian
 import Mathlib.RingTheory.Polynomial.IntegralNormalization
+import Mathlib.RingTheory.Polynomial.Nilpotent
 import Mathlib.RingTheory.Polynomial.Opposites
 import Mathlib.RingTheory.Polynomial.Pochhammer
 import Mathlib.RingTheory.Polynomial.Quotient

Mathlib/Algebra/Regular/Basic.lean

@@ -70,6 +70,8 @@ structure IsRegular (c : R) : Prop where
   right : IsRightRegular c
 #align is_regular IsRegular
 
+attribute [simp] IsRegular.left IsRegular.right
+
 attribute [to_additive] IsRegular
 
 @[to_additive]
@@ -266,6 +268,14 @@ theorem not_isRightRegular_zero [nR : Nontrivial R] : ¬IsRightRegular (0 : R) :
 theorem not_isRegular_zero [Nontrivial R] : ¬IsRegular (0 : R) := fun h => IsRegular.ne_zero h rfl
 #align not_is_regular_zero not_isRegular_zero
 
+@[simp] lemma IsLeftRegular.mul_left_eq_zero_iff (hb : IsLeftRegular b) : b * a = 0 ↔ a = 0 := by
+  nth_rw 1 [← mul_zero b]
+  exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha, mul_zero]⟩
+
+@[simp] lemma IsRightRegular.mul_right_eq_zero_iff (hb : IsRightRegular b) : a * b = 0 ↔ a = 0 := by
+  nth_rw 1 [← zero_mul b]
+  exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha, zero_mul]⟩
+
 end MulZeroClass
 
 section MulOneClass

Mathlib/Data/Nat/SuccPred.lean

@@ -72,6 +72,10 @@ instance : IsSuccArchimedean ℕ :=
 instance : IsPredArchimedean ℕ :=
   ⟨fun {a} {b} h => ⟨b - a, by rw [pred_eq_pred, pred_iterate, tsub_tsub_cancel_of_le h]⟩⟩
 
+lemma forall_ne_zero_iff (P : ℕ → Prop) :
+    (∀ i, i ≠ 0 → P i) ↔ (∀ i, P (i + 1)) :=
+  SuccOrder.forall_ne_bot_iff P
+
 /-! ### Covering relation -/
 
 

Mathlib/Data/Polynomial/Basic.lean

@@ -729,6 +729,9 @@ theorem coeff_C_zero : coeff (C a) 0 = a :=
 theorem coeff_C_ne_zero (h : n ≠ 0) : (C a).coeff n = 0 := by rw [coeff_C, if_neg h]
 #align polynomial.coeff_C_ne_zero Polynomial.coeff_C_ne_zero
 
+@[simp]
+lemma coeff_C_succ {r : R} {n : ℕ} : coeff (C r) (n + 1) = 0 := by simp [coeff_C]
+
 @[simp]
 theorem coeff_nat_cast_ite : (Nat.cast m : R[X]).coeff n = ite (n = 0) m 0 := by
   simp only [← C_eq_nat_cast, coeff_C, Nat.cast_ite, Nat.cast_zero]

Mathlib/Data/Polynomial/Coeff.lean

@@ -6,6 +6,7 @@ Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 import Mathlib.Data.Polynomial.Basic
 import Mathlib.Data.Finset.NatAntidiagonal
 import Mathlib.Data.Nat.Choose.Sum
+import Mathlib.Algebra.Regular.Pow
 
 #align_import data.polynomial.coeff from "leanprover-community/mathlib"@"2651125b48fc5c170ab1111afd0817c903b1fc6c"
 
@@ -179,12 +180,12 @@ theorem coeff_mul_C (p : R[X]) (n : ℕ) (a : R) : coeff (p * C a) n = coeff p n
   exact AddMonoidAlgebra.mul_single_zero_apply p a n
 #align polynomial.coeff_mul_C Polynomial.coeff_mul_C
 
+@[simp]
 theorem coeff_X_pow (k n : ℕ) : coeff (X ^ k : R[X]) n = if n = k then 1 else 0 := by
   simp only [one_mul, RingHom.map_one, ← coeff_C_mul_X_pow]
 #align polynomial.coeff_X_pow Polynomial.coeff_X_pow
 
-@[simp]
-theorem coeff_X_pow_self (n : ℕ) : coeff (X ^ n : R[X]) n = 1 := by simp [coeff_X_pow]
+theorem coeff_X_pow_self (n : ℕ) : coeff (X ^ n : R[X]) n = 1 := by simp
 #align polynomial.coeff_X_pow_self Polynomial.coeff_X_pow_self
 
 section Fewnomials
@@ -293,16 +294,15 @@ theorem mul_X_pow_eq_zero {p : R[X]} {n : ℕ} (H : p * X ^ n = 0) : p = 0 :=
   ext fun k => (coeff_mul_X_pow p n k).symm.trans <| ext_iff.1 H (k + n)
 #align polynomial.mul_X_pow_eq_zero Polynomial.mul_X_pow_eq_zero
 
-theorem mul_X_pow_injective (n : ℕ) : Function.Injective fun P : R[X] => X ^ n * P := by
-  intro P Q hPQ
-  simp only at hPQ
+@[simp] theorem isRegular_X : IsRegular (X : R[X]) := by
+  suffices : IsLeftRegular (X : R[X])
+  · exact ⟨this, this.right_of_commute commute_X⟩
+  intro P Q (hPQ : X * P = X * Q)
   ext i
-  rw [← coeff_X_pow_mul P n i, hPQ, coeff_X_pow_mul Q n i]
-#align polynomial.mul_X_pow_injective Polynomial.mul_X_pow_injective
+  rw [← coeff_X_mul P i, hPQ, coeff_X_mul Q i]
 
-theorem mul_X_injective : Function.Injective fun P : R[X] => X * P :=
-  pow_one (X : R[X]) ▸ mul_X_pow_injective 1
-#align polynomial.mul_X_injective Polynomial.mul_X_injective
+-- TODO Unify this with `Polynomial.Monic.isRegular`
+theorem isRegular_X_pow (n : ℕ) : IsRegular (X ^ n : R[X]) := isRegular_X.pow n
 
 theorem coeff_X_add_C_pow (r : R) (n k : ℕ) :
     ((X + C r) ^ n).coeff k = r ^ (n - k) * (n.choose k : R) := by

Mathlib/Data/Polynomial/Laurent.lean

@@ -605,7 +605,7 @@ theorem isLocalization : IsLocalization (Submonoid.closure ({X} : Set R[X])) R[T
         exact ⟨1, rfl⟩
       · rintro ⟨⟨h, hX⟩, h⟩
         rcases Submonoid.mem_closure_singleton.mp hX with ⟨n, rfl⟩
-        exact mul_X_pow_injective n h }
+        exact (isRegular_X_pow n).left h }
 #align laurent_polynomial.is_localization LaurentPolynomial.isLocalization
 
 end CommSemiring

Mathlib/Data/Polynomial/Reverse.lean

@@ -78,6 +78,8 @@ theorem revAt_le {N i : ℕ} (H : i ≤ N) : revAt N i = N - i :=
   if_pos H
 #align polynomial.rev_at_le Polynomial.revAt_le
 
+lemma revAt_eq_self_of_lt {N i : ℕ} (h : N < i) : revAt N i = i := by simp [revAt, Nat.not_le.mpr h]
+
 theorem revAt_add {N O n o : ℕ} (hn : n ≤ N) (ho : o ≤ O) :
     revAt (N + O) (n + o) = revAt N n + revAt O o := by
   rcases Nat.le.dest hn with ⟨n', rfl⟩

Mathlib/GroupTheory/Submonoid/ZeroDivisors.lean

@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2023 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash
+-/
+import Mathlib.GroupTheory.Submonoid.Basic
+
+/-!
+# Zero divisors
+
+## Main definitions
+
+ * `nonZeroDivisorsLeft`: the elements of a `MonoidWithZero` that are not left zero divisors.
+ * `nonZeroDivisorsRight`: the elements of a `MonoidWithZero` that are not right zero divisors.
+
+-/
+
+section MonoidWithZero
+
+variable (M₀ : Type _) [MonoidWithZero M₀]
+
+/-- The collection of elements of a `MonoidWithZero` that are not left zero divisors form a
+`Submonoid`. -/
+def nonZeroDivisorsLeft : Submonoid M₀ where
+  carrier := {x | ∀ y, y * x = 0 → y = 0}
+  one_mem' := by simp
+  mul_mem' {x} {y} hx hy := fun z hz ↦ hx _ <| hy _ (mul_assoc z x y ▸ hz)
+
+@[simp] lemma mem_nonZeroDivisorsLeft_iff {x : M₀} :
+    x ∈ nonZeroDivisorsLeft M₀ ↔ ∀ y, y * x = 0 → y = 0 :=
+  Iff.rfl
+
+/-- The collection of elements of a `MonoidWithZero` that are not right zero divisors form a
+`Submonoid`. -/
+def nonZeroDivisorsRight : Submonoid M₀ where
+  carrier := {x | ∀ y, x * y = 0 → y = 0}
+  one_mem' := by simp
+  mul_mem' := fun {x} {y} hx hy z hz ↦ hy _ (hx _ ((mul_assoc x y z).symm ▸ hz))
+
+@[simp] lemma mem_nonZeroDivisorsRight_iff {x : M₀} :
+    x ∈ nonZeroDivisorsRight M₀ ↔ ∀ y, x * y = 0 → y = 0 :=
+  Iff.rfl
+
+lemma nonZeroDivisorsLeft_eq_right (M₀ : Type _) [CommMonoidWithZero M₀] :
+    nonZeroDivisorsLeft M₀ = nonZeroDivisorsRight M₀ := by
+  ext x; simp [mul_comm x]
+
+@[simp] lemma coe_nonZeroDivisorsLeft_eq [NoZeroDivisors M₀] [Nontrivial M₀] :
+    nonZeroDivisorsLeft M₀ = {x : M₀ | x ≠ 0} := by
+  ext x
+  simp only [SetLike.mem_coe, mem_nonZeroDivisorsLeft_iff, mul_eq_zero, forall_eq_or_imp, true_and,
+    Set.mem_setOf_eq]
+  refine' ⟨fun h ↦ _, fun hx y hx' ↦ by contradiction⟩
+  contrapose! h
+  exact ⟨1, h, one_ne_zero⟩
+
+@[simp] lemma coe_nonZeroDivisorsRight_eq [NoZeroDivisors M₀] [Nontrivial M₀] :
+    nonZeroDivisorsRight M₀ = {x : M₀ | x ≠ 0} := by
+  ext x
+  simp only [SetLike.mem_coe, mem_nonZeroDivisorsRight_iff, mul_eq_zero, Set.mem_setOf_eq]
+  refine' ⟨fun h ↦ _, fun hx y hx' ↦ by aesop⟩
+  contrapose! h
+  exact ⟨1, Or.inl h, one_ne_zero⟩
+
+end MonoidWithZero

Mathlib/Order/SuccPred/Basic.lean

@@ -1511,3 +1511,14 @@ theorem Pred.rec_top (p : α → Prop) (htop : p ⊤) (hpred : ∀ a, p a → p
 #align pred.rec_top Pred.rec_top
 
 end OrderTop
+
+lemma SuccOrder.forall_ne_bot_iff
+    [Nontrivial α] [PartialOrder α] [OrderBot α] [SuccOrder α] [IsSuccArchimedean α]
+    (P : α → Prop) :
+    (∀ i, i ≠ ⊥ → P i) ↔ (∀ i, P (SuccOrder.succ i)) := by
+  refine' ⟨fun h i ↦ h _ (Order.succ_ne_bot i), fun h i hi ↦ _⟩
+  obtain ⟨j, rfl⟩ := exists_succ_iterate_of_le (bot_le : ⊥ ≤ i)
+  have hj : 0 < j := by apply Nat.pos_of_ne_zero; contrapose! hi; simp [hi]
+  rw [← Nat.succ_pred_eq_of_pos hj]
+  simp only [Function.iterate_succ', Function.comp_apply]
+  apply h

Mathlib/RingTheory/Nilpotent.lean

@@ -5,6 +5,7 @@ Authors: Oliver Nash
 -/
 import Mathlib.Data.Nat.Choose.Sum
 import Mathlib.Algebra.Algebra.Bilinear
+import Mathlib.GroupTheory.Submonoid.ZeroDivisors
 import Mathlib.RingTheory.Ideal.Operations
 import Mathlib.Algebra.GeomSum
 
@@ -43,7 +44,7 @@ theorem IsNilpotent.mk [Zero R] [Pow R ℕ] (x : R) (n : ℕ) (e : x ^ n = 0) :
   ⟨n, e⟩
 #align is_nilpotent.mk IsNilpotent.mk
 
-theorem IsNilpotent.zero [MonoidWithZero R] : IsNilpotent (0 : R) :=
+@[simp] theorem IsNilpotent.zero [MonoidWithZero R] : IsNilpotent (0 : R) :=
   ⟨1, pow_one 0⟩
 #align is_nilpotent.zero IsNilpotent.zero
 
@@ -172,17 +173,43 @@ theorem isNilpotent_add (hx : IsNilpotent x) (hy : IsNilpotent y) : IsNilpotent
   · rw [pow_eq_zero_of_le hj hm, MulZeroClass.mul_zero]
 #align commute.is_nilpotent_add Commute.isNilpotent_add
 
+protected lemma isNilpotent_sum {ι : Type _} {s : Finset ι} {f : ι → R}
+    (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ i j, i ∈ s → j ∈ s → Commute (f i) (f j)) :
+    IsNilpotent (∑ i in s, f i) := by
+  classical
+  induction' s using Finset.induction with j s hj ih; simp
+  rw [Finset.sum_insert hj]
+  apply Commute.isNilpotent_add
+  · exact Commute.sum_right _ _ _ (fun i hi ↦ h_comm _ _ (by simp) (by simp [hi]))
+  · apply hnp; simp
+  · exact ih (fun i hi ↦ hnp i (by simp [hi]))
+      (fun i j hi hj ↦ h_comm i j (by simp [hi]) (by simp [hj]))
+
 theorem isNilpotent_mul_left (h : IsNilpotent x) : IsNilpotent (x * y) := by
   obtain ⟨n, hn⟩ := h
   use n
   rw [h_comm.mul_pow, hn, MulZeroClass.zero_mul]
 #align commute.is_nilpotent_mul_left Commute.isNilpotent_mul_left
 
+protected lemma isNilpotent_mul_left_iff (hy : y ∈ nonZeroDivisorsLeft R) :
+    IsNilpotent (x * y) ↔ IsNilpotent x := by
+  refine' ⟨_, h_comm.isNilpotent_mul_left⟩
+  rintro ⟨k, hk⟩
+  rw [mul_pow h_comm] at hk
+  exact ⟨k, (nonZeroDivisorsLeft R).pow_mem hy k _ hk⟩
+
 theorem isNilpotent_mul_right (h : IsNilpotent y) : IsNilpotent (x * y) := by
   rw [h_comm.eq]
   exact h_comm.symm.isNilpotent_mul_left h
 #align commute.is_nilpotent_mul_right Commute.isNilpotent_mul_right
 
+protected lemma isNilpotent_mul_right_iff (hx : x ∈ nonZeroDivisorsRight R) :
+    IsNilpotent (x * y) ↔ IsNilpotent y := by
+  refine' ⟨_, h_comm.isNilpotent_mul_right⟩
+  rintro ⟨k, hk⟩
+  rw [mul_pow h_comm] at hk
+  exact ⟨k, (nonZeroDivisorsRight R).pow_mem hx k _ hk⟩
+
 end Semiring
 
 section Ring
@@ -202,7 +229,12 @@ end Commute
 
 section CommSemiring
 
-variable [CommSemiring R]
+variable [CommSemiring R] {x y : R}
+
+lemma isNilpotent_sum {ι : Type _} {s : Finset ι} {f : ι → R}
+    (hnp : ∀ i ∈ s, IsNilpotent (f i)) :
+    IsNilpotent (∑ i in s, f i) :=
+  Commute.isNilpotent_sum hnp fun _ _ _ _ ↦ Commute.all _ _
 
 /-- The nilradical of a commutative semiring is the ideal of nilpotent elements. -/
 def nilradical (R : Type _) [CommSemiring R] : Ideal R :=