posFittingComp_eq_bot_of_isNilpotent

Mathlib.Algebra.Lie.Weights.Basic

URI: https://scilib.ai/kg/mathlib#LieModule.posFittingComp_eq_bot_of_isNilpotent

English

If L is nilpotent and M is nilpotent as a Lie module, then posFittingComp is the zero submodule.

Русский

Если L ниlпотent и M является нильпотентным модулем Ли, то posFittingComp = ⊥.

LaTeX

$$$\operatorname{posFittingComp}(R,L,M) = \bot$$$

Lean4

@[simp]
theorem posFittingComp_eq_bot_of_isNilpotent [IsNilpotent L M] : posFittingComp R L M = ⊥ := by simp [posFittingComp]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru