nilpotencyLength_eq_one_iff — Mathlib

English

If M is nontrivial, then nilpotencyLength L M = 1 if and only if the action of L on M is trivial.

Русский

Если M ненулевой, то nilpotencyLength L M = 1 тогда и только тогда, когда действие L на M тривиально.

LaTeX

$$$[\\text{Nontrivial}(M)] \\Rightarrow (\\ nilpotencyLength(L,M) = 1 \\\\iff \\ IsTrivial_L(M)).$$$

Lean4

@[simp]
theorem nilpotencyLength_eq_one_iff [Nontrivial M] : nilpotencyLength L M = 1 ↔ IsTrivial L M :=
  by
  rw [nilpotencyLength_eq_succ_iff ℤ, ← trivial_iff_lower_central_eq_bot]
  simp

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