nilpotencyClass_eq_succ_iff — Mathlib

English

For a fixed 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

$$$\\forall k:\\mathbb{N},\\ nilpotencyClass\_x = k+1 \\iff x^{k+1}=0 \\land x^k \\neq 0$$$

Lean4

theorem nilpotencyClass_eq_succ_iff {k : ℕ} : nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0 :=
  by
  let s : Set ℕ := {k | x ^ k = 0}
  have : ∀ k₁ k₂ : ℕ, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s := fun k₁ k₂ h_le hk₁ ↦ pow_eq_zero_of_le h_le hk₁
  simp [s, nilpotencyClass, Nat.sInf_upward_closed_eq_succ_iff this]

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