lieModuleIsNilpotent — Mathlib

English

A simple specialization of the LCS map inequality that follows from basic properties of Submodule mappings.

Русский

Упрощённая форма неравенства отображения нижней центральной серии как следствие базовых свойств отображения подмодулей.

LaTeX

$$∀ {R} {L} {M} [..], (lowerCentralSeries_simp1) → …$$

Lean4

theorem lieModuleIsNilpotent [IsNilpotent L₂ M₂] : IsNilpotent L M :=
  by
  obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R L₂ M₂
  rw [isNilpotent_iff R]
  use k
  rw [← LieSubmodule.toSubmodule_inj] at hk ⊢
  apply Submodule.map_injective_of_injective hg_inj
  simpa [hk] using lieModule_lcs_map_le hfg k

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