English
If R acts on a nontrivial M with NoZeroSmulDivisors, then R has no nonzero nilpotent elements; equivalently, R is reduced.
Русский
Если кольцо R действует на ненулевой модуль M с свойством NoZeroSmulDivisors, то в R нет ненулевых нилпотентных элементов; иначе говоря, R редуцирован.
LaTeX
$$$ \\text{IsReduced}(R) $$$
Lean4
theorem 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
| zero =>
rw [pow_zero] at hk
exact eq_zero_of_zero_eq_one hk.symm x
| succ k ih =>
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
