instIsLieTowerSubtypeMemLieSubmodule

Mathlib.Algebra.Lie.Ideal

URI: https://scilib.ai/kg/mathlib#instIsLieTowerSubtypeMemLieSubmodule

English

There is a LieTower instance on the subtype {x ∈ L | x ∈ I} viewed as a LieSubmodule over M.

Русский

Существует экземпляр IsLieTower для подтипа {x ∈ L | x ∈ I}, рассматриваемого как LieSubmodule над M.

LaTeX

$$$ \text{IsLieTower}\bigl(\text{Subtype}(x\in I)\bigr)\; L\; M $$$

Lean4

instance (I : LieIdeal R L) : IsLieTower I L M where leibniz_lie x y m := leibniz_lie x.val y m

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

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

Разделы

Аффилиация

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