feat: basic lemmas about nilpotency in rings (#8156)

Mathlib/RingTheory/Nilpotent.lean

@@ -78,6 +78,11 @@ theorem IsNilpotent.map [MonoidWithZero R] [MonoidWithZero S] {r : R} {F : Type*
   rw [← map_pow, hr.choose_spec, map_zero]
 #align is_nilpotent.map IsNilpotent.map
 
+lemma IsNilpotent.map_iff [MonoidWithZero R] [MonoidWithZero S] {r : R} {F : Type*}
+    [MonoidWithZeroHomClass F R S] {f : F} (hf : Function.Injective f) :
+    IsNilpotent (f r) ↔ IsNilpotent r :=
+  ⟨fun ⟨k, hk⟩ ↦ ⟨k, (map_eq_zero_iff f hf).mp <| by rwa [map_pow]⟩, fun h ↦ h.map f⟩
+
 theorem IsNilpotent.sub_one_isUnit [Ring R] {r : R} (hnil : IsNilpotent r) : IsUnit (r - 1) := by
   obtain ⟨n, hn⟩ := hnil
   refine' ⟨⟨r - 1, -∑ i in Finset.range n, r ^ i, _, _⟩, rfl⟩
@@ -322,3 +327,16 @@ theorem IsNilpotent.mapQ (hnp : IsNilpotent f) : IsNilpotent (p.mapQ p f hp) :=
 #align module.End.is_nilpotent.mapq Module.End.IsNilpotent.mapQ
 
 end Module.End
+
+lemma NoZeroSMulDivisors.isReduced (R M : Type*)
+    [MonoidWithZero R] [Zero M] [MulActionWithZero R M] [Nontrivial M] [NoZeroSMulDivisors R M] :
+    IsReduced R := by
+  refine ⟨fun x ⟨k, hk⟩ ↦ ?_⟩
+  induction' k with k ih
+  · rw [Nat.zero_eq, pow_zero] at hk
+    exact eq_zero_of_zero_eq_one hk.symm x
+  · obtain ⟨m : M, hm : m ≠ 0⟩ := exists_ne (0 : M)
+    have : x ^ (k + 1) • m = 0 := by simp only [hk, zero_smul]
+    rw [pow_succ, mul_smul] at this
+    rcases eq_zero_or_eq_zero_of_smul_eq_zero this with rfl | hx; rfl
+    exact ih <| (eq_zero_or_eq_zero_of_smul_eq_zero hx).resolve_right hm