lowerCentralSeriesLast_le_of_not_isTrivial

English

If the module is not trivial, then the last nontrivial term bounds the first nontrivial term: Last ≤ lcs 1.

Русский

Если модуль не тривиален, то последний ненулевой член ограничивает первый ненулевой член: Last ≤ lcs 1.

LaTeX

$$$\\text{NotIsTrivial}(L,M) \\Rightarrow \\text{lowerCentralSeriesLast}(R,L,M) \\le \\lowerCentralSeries R L M 1.$$$

Lean4

theorem lowerCentralSeriesLast_le_of_not_isTrivial [IsNilpotent L M] (h : ¬IsTrivial L M) :
    lowerCentralSeriesLast R L M ≤ lowerCentralSeries R L M 1 :=
  by
  rw [lowerCentralSeriesLast]
  replace h : 1 < nilpotencyLength L M := by
    by_contra contra
    have := isTrivial_of_nilpotencyLength_le_one L M (not_lt.mp contra)
    contradiction
  rcases hk : nilpotencyLength L M with - | k <;> rw [hk] at h
  · contradiction
  · exact antitone_lowerCentralSeries _ _ _ (Nat.lt_succ.mp h)

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