English
If M is nilpotent, then nilpotencyLength L M = 0 if and only if M is subsingleton.
Русский
Если M нильпотентен, то nilpotencyLength L M = 0 тогда и только тогда, когда M является одиночным множеством.
LaTeX
$$$[\\text{IsNilpotent}_L(M)] \\Rightarrow (\\ nilpotencyLength(L,M) = 0 \\iff M \\text{ is a subsingleton}).$$$
Lean4
@[simp]
theorem nilpotencyLength_eq_zero_iff [IsNilpotent L M] : nilpotencyLength L M = 0 ↔ Subsingleton M :=
by
let s := {k | lowerCentralSeries ℤ L M k = ⊥}
have hs : s.Nonempty := by
obtain ⟨k, hk⟩ := IsNilpotent.nilpotent ℤ L M
exact ⟨k, hk⟩
change sInf s = 0 ↔ _
rw [← LieSubmodule.subsingleton_iff ℤ L M, ← subsingleton_iff_bot_eq_top, ← lowerCentralSeries_zero,
@eq_comm (LieSubmodule ℤ L M)]
refine ⟨fun h => h ▸ Nat.sInf_mem hs, fun h => ?_⟩
rw [Nat.sInf_eq_zero]
exact Or.inl h
