instIsLieTowerSubtypeMem — Mathlib

English

If M is a Lie L-module, then restricting scalars to the Lie subalgebra L' ⊆ L yields a Lie L'-module structure on M.

Русский

Если M — модуль по Ли-алгебре L, то ограничение по подалгебре L' ⊆ L даёт структуру модуля Ли над L'.

LaTeX

$$$$\text{IsLieTower }(\text{Subtype }(\lambda x: x \in L')), L, M.$$$$

Lean4

instance : IsLieTower L' L M where leibniz_lie x y m := leibniz_lie x.val y m

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