feat: lemmas about divisibility, mostly related to nilpotency (#7355)

Mathlib.lean

@@ -418,7 +418,8 @@ import Mathlib.Algebra.Ring.BooleanRing
 import Mathlib.Algebra.Ring.Commute
 import Mathlib.Algebra.Ring.CompTypeclasses
 import Mathlib.Algebra.Ring.Defs
-import Mathlib.Algebra.Ring.Divisibility
+import Mathlib.Algebra.Ring.Divisibility.Basic
+import Mathlib.Algebra.Ring.Divisibility.Lemmas
 import Mathlib.Algebra.Ring.Equiv
 import Mathlib.Algebra.Ring.Fin
 import Mathlib.Algebra.Ring.Idempotents

Mathlib/Algebra/BigOperators/Multiset/Basic.lean

@@ -342,17 +342,17 @@ theorem sum_map_mul_right : sum (s.map fun i => f i * a) = sum (s.map f) * a :=
 
 end NonUnitalNonAssocSemiring
 
-section Semiring
+section NonUnitalSemiring
 
-variable [Semiring α]
+variable [NonUnitalSemiring α]
 
 theorem dvd_sum {a : α} {s : Multiset α} : (∀ x ∈ s, a ∣ x) → a ∣ s.sum :=
   Multiset.induction_on s (fun _ => dvd_zero _) fun x s ih h => by
     rw [sum_cons]
     exact dvd_add (h _ (mem_cons_self _ _)) (ih fun y hy => h _ <| mem_cons.2 <| Or.inr hy)
 #align multiset.dvd_sum Multiset.dvd_sum
 
-end Semiring
+end NonUnitalSemiring
 
 /-! ### Order -/
 

Mathlib/Algebra/BigOperators/Ring.lean

@@ -68,6 +68,11 @@ end Semiring
 
 section Semiring
 
+theorem dvd_sum [NonUnitalSemiring β]
+    {b : β} {s : Finset α} {f : α → β} (h : ∀ x ∈ s, b ∣ f x) : b ∣ ∑ x in s, f x :=
+  Multiset.dvd_sum fun y hy => by rcases Multiset.mem_map.1 hy with ⟨x, hx, rfl⟩; exact h x hx
+#align finset.dvd_sum Finset.dvd_sum
+
 variable [NonAssocSemiring β]
 
 theorem sum_mul_boole [DecidableEq α] (s : Finset α) (f : α → β) (a : α) :
@@ -209,10 +214,6 @@ theorem sum_pow_mul_eq_add_pow {α R : Type*} [CommSemiring R] (a b : R) (s : Fi
   rw [prod_const, prod_const, ← card_sdiff (mem_powerset.1 ht)]
 #align finset.sum_pow_mul_eq_add_pow Finset.sum_pow_mul_eq_add_pow
 
-theorem dvd_sum {b : β} {s : Finset α} {f : α → β} (h : ∀ x ∈ s, b ∣ f x) : b ∣ ∑ x in s, f x :=
-  Multiset.dvd_sum fun y hy => by rcases Multiset.mem_map.1 hy with ⟨x, hx, rfl⟩; exact h x hx
-#align finset.dvd_sum Finset.dvd_sum
-
 @[norm_cast]
 theorem prod_natCast (s : Finset α) (f : α → ℕ) : ↑(∏ x in s, f x : ℕ) = ∏ x in s, (f x : β) :=
   (Nat.castRingHom β).map_prod f s

Mathlib/Algebra/EuclideanDomain/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Louis Carlin, Mario Carneiro
 -/
 import Mathlib.Algebra.EuclideanDomain.Defs
-import Mathlib.Algebra.Ring.Divisibility
+import Mathlib.Algebra.Ring.Divisibility.Basic
 import Mathlib.Algebra.Ring.Regular
 import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Algebra.Ring.Basic

Mathlib/Algebra/GroupPower/Ring.lean

@@ -10,7 +10,7 @@ import Mathlib.Algebra.Hom.Ring.Defs
 import Mathlib.Algebra.Hom.Units
 import Mathlib.Algebra.Ring.Commute
 import Mathlib.Algebra.GroupWithZero.Divisibility
-import Mathlib.Algebra.Ring.Divisibility
+import Mathlib.Algebra.Ring.Divisibility.Basic
 import Mathlib.Data.Nat.Order.Basic
 
 #align_import algebra.group_power.ring from "leanprover-community/mathlib"@"fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e"
@@ -199,6 +199,9 @@ theorem neg_pow (a : R) (n : ℕ) : (-a) ^ n = (-1) ^ n * a ^ n :=
   neg_one_mul a ▸ (Commute.neg_one_left a).mul_pow n
 #align neg_pow neg_pow
 
+theorem neg_pow' (a : R) (n : ℕ) : (-a) ^ n = a ^ n * (-1) ^ n :=
+  mul_neg_one a ▸ (Commute.neg_one_right a).mul_pow n
+
 section
 set_option linter.deprecated false
 

Mathlib/Algebra/Order/Ring/Abs.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
 -/
 import Mathlib.Algebra.Order.Ring.Defs
-import Mathlib.Algebra.Ring.Divisibility
+import Mathlib.Algebra.Ring.Divisibility.Basic
 import Mathlib.Algebra.Order.Group.Abs
 
 #align_import algebra.order.ring.abs from "leanprover-community/mathlib"@"10b4e499f43088dd3bb7b5796184ad5216648ab1"

Mathlib/Algebra/Ring/Divisibility.lean → Mathlib/Algebra/Ring/Divisibility/Basic.lean

@@ -11,6 +11,10 @@ import Mathlib.Algebra.Ring.Defs
 
 /-!
 # Lemmas about divisibility in rings
+
+Note that this file is imported by basic tactics like `linarith` and so must have only minimal
+imports. Further results about divisibility in rings may be found in
+`Mathlib.Algebra.Ring.Divisibility.Lemmas` which is not subject to this import constraint.
 -/
 
 

Mathlib/Algebra/Ring/Divisibility/Lemmas.lean

@@ -0,0 +1,91 @@
+/-
+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.Algebra.Ring.Divisibility.Basic
+import Mathlib.Data.Nat.Choose.Sum
+
+/-!
+# Lemmas about divisibility in rings
+
+## Main results:
+* `dvd_smul_of_dvd`: stating that `x ∣ y → x ∣ m • y` for any scalar `m`.
+* `Commute.pow_dvd_add_pow_of_pow_eq_zero_right`: stating that if `y` is nilpotent then
+  `x ^ m ∣ (x + y) ^ p` for sufficiently large `p` (together with many variations for convenience).
+-/
+
+variable {R : Type*}
+
+lemma dvd_smul_of_dvd {M : Type*} [SMul M R] [Semigroup R] [SMulCommClass M R R] {x y : R}
+    (m : M) (h : x ∣ y) : x ∣ m • y :=
+  let ⟨k, hk⟩ := h; ⟨m • k, by rw [mul_smul_comm, ← hk]⟩
+
+lemma dvd_nsmul_of_dvd [NonUnitalSemiring R] {x y : R} (n : ℕ) (h : x ∣ y) : x ∣ n • y :=
+  dvd_smul_of_dvd n h
+
+lemma dvd_zsmul_of_dvd [NonUnitalRing R] {x y : R} (z : ℤ) (h : x ∣ y) : x ∣ z • y :=
+  dvd_smul_of_dvd z h
+
+namespace Commute
+
+variable {x y : R} {n m p : ℕ} (hp : n + m ≤ p + 1)
+
+section Semiring
+
+variable [Semiring R] (h_comm : Commute x y)
+
+lemma pow_dvd_add_pow_of_pow_eq_zero_right (hy : y ^ n = 0) :
+    x ^ m ∣ (x + y) ^ p := by
+  rw [h_comm.add_pow']
+  refine Finset.dvd_sum fun ⟨i, j⟩ hij ↦ ?_
+  replace hij : i + j = p := by simpa using hij
+  apply dvd_nsmul_of_dvd
+  rcases le_or_lt m i with (hi : m ≤ i) | (hi : i + 1 ≤ m)
+  · exact dvd_mul_of_dvd_left (pow_dvd_pow x hi) _
+  · simp [pow_eq_zero_of_le (by linarith : n ≤ j) hy]
+
+lemma pow_dvd_add_pow_of_pow_eq_zero_left (hx : x ^ n = 0) :
+    y ^ m ∣ (x + y) ^ p :=
+  add_comm x y ▸ h_comm.symm.pow_dvd_add_pow_of_pow_eq_zero_right hp hx
+
+end Semiring
+
+section Ring
+
+variable [Ring R] (h_comm : Commute x y)
+
+lemma pow_dvd_pow_of_sub_pow_eq_zero (h : (x - y) ^ n = 0) :
+    x ^ m ∣ y ^ p := by
+  rw [← sub_add_cancel y x]
+  apply (h_comm.symm.sub_left rfl).pow_dvd_add_pow_of_pow_eq_zero_left hp _
+  rw [← neg_sub x y, neg_pow, h, mul_zero]
+
+lemma pow_dvd_pow_of_add_pow_eq_zero (h : (x + y) ^ n = 0) :
+    x ^ m ∣ y ^ p := by
+  rw [← neg_neg y, neg_pow']
+  apply dvd_mul_of_dvd_left
+  apply h_comm.neg_right.pow_dvd_pow_of_sub_pow_eq_zero hp
+  simpa
+
+lemma pow_dvd_sub_pow_of_pow_eq_zero_right (hy : y ^ n = 0) :
+    x ^ m ∣ (x - y) ^ p :=
+  (sub_right rfl h_comm).pow_dvd_pow_of_sub_pow_eq_zero hp (by simpa)
+
+lemma pow_dvd_sub_pow_of_pow_eq_zero_left (hx : x ^ n = 0) :
+    y ^ m ∣ (x - y) ^ p := by
+  rw [← neg_sub y x, neg_pow']
+  apply dvd_mul_of_dvd_left
+  exact h_comm.symm.pow_dvd_sub_pow_of_pow_eq_zero_right hp hx
+
+lemma add_pow_dvd_pow_of_pow_eq_zero_right (hx : x ^ n = 0) :
+    (x + y) ^ m ∣ y ^ p :=
+  (h_comm.add_left rfl).pow_dvd_pow_of_sub_pow_eq_zero hp (by simpa)
+
+lemma add_pow_dvd_pow_of_pow_eq_zero_left (hy : y ^ n = 0) :
+    (x + y) ^ m ∣ x ^ p :=
+  add_comm x y ▸ h_comm.symm.add_pow_dvd_pow_of_pow_eq_zero_right hp hy
+
+end Ring
+
+end Commute

Mathlib/Data/Int/Order/Basic.lean

@@ -5,7 +5,7 @@ Authors: Jeremy Avigad
 -/
 
 import Mathlib.Data.Int.Basic
-import Mathlib.Algebra.Ring.Divisibility
+import Mathlib.Algebra.Ring.Divisibility.Basic
 import Mathlib.Algebra.Order.Group.Abs
 import Mathlib.Algebra.Order.Ring.CharZero
 

Mathlib/Data/List/BigOperators/Lemmas.lean

@@ -11,7 +11,7 @@ import Mathlib.Algebra.GroupWithZero.Commute
 import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Algebra.Order.WithZero
 import Mathlib.Algebra.Ring.Basic
-import Mathlib.Algebra.Ring.Divisibility
+import Mathlib.Algebra.Ring.Divisibility.Basic
 import Mathlib.Algebra.Ring.Commute
 import Mathlib.Data.Int.Units
 import Mathlib.Data.Set.Basic
@@ -85,7 +85,7 @@ theorem dvd_prod [CommMonoid M] {a} {l : List M} (ha : a ∈ l) : a ∣ l.prod :
   exact dvd_mul_right _ _
 #align list.dvd_prod List.dvd_prod
 
-theorem dvd_sum [Semiring R] {a} {l : List R} (h : ∀ x ∈ l, a ∣ x) : a ∣ l.sum := by
+theorem dvd_sum [NonUnitalSemiring R] {a} {l : List R} (h : ∀ x ∈ l, a ∣ x) : a ∣ l.sum := by
   induction' l with x l ih
   · exact dvd_zero _
   · rw [List.sum_cons]

Mathlib/Data/Nat/Order/Lemmas.lean

@@ -6,7 +6,7 @@ Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 import Mathlib.Data.Nat.Order.Basic
 import Mathlib.Data.Nat.Units
 import Mathlib.Data.Set.Basic
-import Mathlib.Algebra.Ring.Divisibility
+import Mathlib.Algebra.Ring.Divisibility.Basic
 import Mathlib.Algebra.GroupWithZero.Divisibility
 
 #align_import data.nat.order.lemmas from "leanprover-community/mathlib"@"e8638a0fcaf73e4500469f368ef9494e495099b3"

Mathlib/RingTheory/Coprime/Basic.lean

@@ -5,7 +5,7 @@ Authors: Kenny Lau, Ken Lee, Chris Hughes
 -/
 import Mathlib.Tactic.Ring
 import Mathlib.GroupTheory.GroupAction.Units
-import Mathlib.Algebra.Ring.Divisibility
+import Mathlib.Algebra.Ring.Divisibility.Basic
 import Mathlib.Algebra.Hom.Ring.Defs
 import Mathlib.Algebra.GroupPower.Ring