isNilpotent_iff_zero_mem_powers — Mathlib

English

In a Monoid with zero, x is nilpotent if and only if 0 belongs to the powers of x, i.e., ∃ n with x^n = 0.

Русский

В моноиде с нулём элемент $x$ нильпотентен тогда и только тогда, когда 0 принадлежит степеням $x$, т.е. существует $n$, такое что $x^n = 0$.

LaTeX

$$$IsNilpotent(x) \iff 0 \in \operatorname{powers}(x)$$$

Lean4

theorem isNilpotent_iff_zero_mem_powers [Monoid R] [Zero R] {x : R} : IsNilpotent x ↔ 0 ∈ Submonoid.powers x :=
  Iff.rfl

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