isNilpotent_of_pos_nilpotencyClass

English

For any k, nilpotencyClass(x) = k+1 if and only if x^(k+1) = 0 and x^k ≠ 0.

Русский

Для любого k: nilpotencyClass(x) = k+1 тогда и только тогда, когда x^(k+1) = 0 и x^k ≠ 0.

LaTeX

$$$ nilpotencyClass(x) = k+1 \\iff (x^{k+1}=0) \\land (x^k \\neq 0) $$$

Lean4

theorem isNilpotent_of_pos_nilpotencyClass (hx : 0 < nilpotencyClass x) : IsNilpotent x :=
  by
  let s : Set ℕ := {k | x ^ k = 0}
  change s.Nonempty
  change 0 < sInf s at hx
  by_contra contra
  simp [not_nonempty_iff_eq_empty.mp contra] at hx

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