lowerCentralSeriesLast_le_max_triv

English

The last term in the nontrivial nilpotent filtration is contained in the maximal trivial submodule.

Русский

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

LaTeX

$$$\\text{lowerCentralSeriesLast}(R,L,M) \\le \\maxTrivSubmodule(R,L,M).$$$

Lean4

theorem lowerCentralSeriesLast_le_max_triv [LieModule R L M] : lowerCentralSeriesLast R L M ≤ maxTrivSubmodule R L M :=
  by
  rw [lowerCentralSeriesLast]
  rcases h : nilpotencyLength L M with - | k
  · exact bot_le
  · rw [le_max_triv_iff_bracket_eq_bot]
    rw [nilpotencyLength_eq_succ_iff R, lowerCentralSeries_succ] at h
    exact h.1

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