English
For any k, nilpotencyLength L M = k+1 if and only if the k+1-th lower central series is zero and the k-th one is nonzero.
Русский
Для любого k: nilpotencyLength L M = k+1 тогда и только тогда, когда (k+1)-я нижняя центральная серия равна нулю, а k-я ненулевая.
LaTeX
$$$\\text{nilpotencyLength}(L,M) = k+1 \\iff \\lowerCentralSeries_R L M (k+1) = ⊥ \\land \\lowerCentralSeries_R L M k \\neq ⊥.$$$
Lean4
theorem nilpotencyLength_eq_succ_iff (k : ℕ) :
nilpotencyLength L M = k + 1 ↔ lowerCentralSeries R L M (k + 1) = ⊥ ∧ lowerCentralSeries R L M k ≠ ⊥ :=
by
have aux (k : ℕ) : lowerCentralSeries R L M k = ⊥ ↔ lowerCentralSeries ℤ L M k = ⊥ := by
simp [SetLike.ext'_iff, coe_lowerCentralSeries_eq_int R L M]
let s := {k | lowerCentralSeries ℤ L M k = ⊥}
rw [aux, ne_eq, aux]
change sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
have hs : ∀ k₁ k₂, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s :=
by
rintro k₁ k₂ h₁₂ (h₁ : lowerCentralSeries ℤ L M k₁ = ⊥)
exact eq_bot_iff.mpr (h₁ ▸ antitone_lowerCentralSeries ℤ L M h₁₂)
exact Nat.sInf_upward_closed_eq_succ_iff hs k
