eq_zero_of_isNilpotent — Mathlib

English

If e is an idempotent element and nilpotent in a monoid with zero, then e = 0.

Русский

Если e идемпотентный элемент и нильпотентен, то e = 0.

LaTeX

$$$ \\text{IsIdempotentElem}(e) \\land \\text{IsNilpotent}(e) \\Rightarrow e = 0 $$$

Lean4

theorem eq_zero_of_isNilpotent [MonoidWithZero R] {e : R} (idem : IsIdempotentElem e) (nilp : IsNilpotent e) : e = 0 :=
  by
  obtain ⟨rfl | n, hn⟩ := nilp
  · rw [pow_zero] at hn; rw [← one_mul e, hn, zero_mul]
  · rw [← hn, idem.pow_succ_eq]

Похожие утверждения