coe_lcs_range_toEnd_eq — Mathlib

English

If M is nontrivial and nilpotent, then the maximal trivial submodule inside M is itself nontrivial.

Русский

Если M не тривиален и нильпотентен, то максимальное тривиальное подмодуль внутри M также не тривиально.

LaTeX

$$[\\text{Nontrivial }M] [\\text{IsNilpotent}_L(M)] \\Rightarrow \\operatorname{Nontrivial}(\\maxTrivSubmodule R L M).$$

Lean4

@[simp]
theorem coe_lcs_range_toEnd_eq (k : ℕ) :
    (lowerCentralSeries R (toEnd R L M).range M k : Submodule R M) = lowerCentralSeries R L M k := by
  induction k with
  | zero => simp
  | succ k
    ih =>
    simp only [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span',
      ← (lowerCentralSeries R (toEnd R L M).range M k).mem_toSubmodule, ih]
    simp

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