nontrivial_lowerCentralSeriesLast

English

Under the hypotheses of nilpotence and nontrivial M, the last nontrivial term of the lower central series is nontrivial.

Русский

При условии нильпотентности и ненулевого M последний ненулевой член нижней центральной серии не тривиален.

LaTeX

$$$[\\text{Nontrivial}(M)] \\land [\\text{IsNilpotent}_L(M)] \\Rightarrow \\text{Nontrivial}(\\text{lowerCentralSeriesLast}(R,L,M)).$$$

Lean4

theorem nontrivial_lowerCentralSeriesLast [LieModule R L M] [Nontrivial M] [IsNilpotent L M] :
    Nontrivial (lowerCentralSeriesLast R L M) :=
  by
  rw [LieSubmodule.nontrivial_iff_ne_bot, lowerCentralSeriesLast]
  cases h : nilpotencyLength L M
  · rw [nilpotencyLength_eq_zero_iff, ← not_nontrivial_iff_subsingleton] at h
    contradiction
  · rw [nilpotencyLength_eq_succ_iff R] at h
    exact h.2

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