instIsNilpotentSubtypeMemLieSubmoduleOfIsNilpotent

English

If IsNilpotent L I as a Lie module, then the Lie ring IsNilpotent structure on the subtype I is inherited, i.e., I is nilpotent as a Lie ring.

Русский

Если I является нильпотентным как модуль Ли над L, то I как круг Ли также нильпотентен.

LaTeX

$$[IsNilpotent L I] ⇒ LieRing.IsNilpotent I$$

Lean4

instance [IsNilpotent L I] : LieRing.IsNilpotent I :=
  by
  let f : I →ₗ⁅R⁆ L := I.incl
  let g : I →ₗ⁅R⁆ I := LieHom.id
  have hfg : ∀ x m, ⁅f x, g m⁆ = g ⁅x, m⁆ := by aesop
  exact Function.injective_id.lieModuleIsNilpotent hfg

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