pos_nilpotencyClass_iff — Mathlib

English

Let R be a nontrivial monoid with zero. For every x ∈ R, x is nilpotent if and only if its nilpotency class is positive.

Русский

Пусть R — ненулевой моноид с нулём. Для любого элемента x ∈ R выполняется: x нильпотентен тогда и только тогда, когда его нильпотентная степень (nilpotencyClass) положительна.

LaTeX

$$$0 < \mathrm{nilpotencyClass}(x) \iff \mathrm{IsNilpotent}(x)$$$

Lean4

@[simp]
theorem pos_nilpotencyClass_iff [Nontrivial R] : 0 < nilpotencyClass x ↔ IsNilpotent x :=
  by
  refine ⟨isNilpotent_of_pos_nilpotencyClass, fun hx ↦ Nat.pos_of_ne_zero fun hx' ↦ ?_⟩
  replace hx := pow_nilpotencyClass hx
  rw [hx', pow_zero] at hx
  exact one_ne_zero hx

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