pow_pred_nilpotencyClass — Mathlib

English

If x is nilpotent, then x raised to the power (nilpotencyClass(x) − 1) is nonzero.

Русский

Если x нильпотентен, то x^{nilpotencyClass(x) − 1} ≠ 0.

LaTeX

$$$\mathrm{IsNilpotent}(x) \Rightarrow x^{\mathrm{nilpotencyClass}(x) - 1} \neq 0$$$

Lean4

theorem pow_pred_nilpotencyClass [Nontrivial R] (hx : IsNilpotent x) : x ^ (nilpotencyClass x - 1) ≠ 0 :=
  (nilpotencyClass_eq_succ_iff.mp <| Nat.eq_add_of_sub_eq (pos_nilpotencyClass_iff.mpr hx) rfl).2

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