instMaxNilpotentSubmoduleIsNilpotent

English

Under Noetherian hypothesis on M, the maximal nilpotent submodule is itself nilpotent as a Lie module.

Русский

При условии, что M удовлетворяет теореме Нейтер, максимальный нильпотентный подмодуль сам по себе нильпотентен как Ли-модуль.

LaTeX

$$IsNilpotent L (maxNilpotentSubmodule R L M)$$

Lean4

instance instMaxNilpotentSubmoduleIsNilpotent [IsNoetherian R M] : IsNilpotent L (maxNilpotentSubmodule R L M) :=
  by
  have hwf := CompleteLattice.WellFoundedGT.isSupClosedCompact (LieSubmodule R L M) inferInstance
  refine hwf {N : LieSubmodule R L M | IsNilpotent L N} ⟨⊥, ?_⟩ fun N₁ h₁ N₂ h₂ => ?_ <;> simp_all <;> infer_instance

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