English
Given a Lie subalgebra L' ⊆ L and a Lie module M over L, M becomes a Lie module over L' by restriction of the action.
Русский
Для подалгебры L' ⊆ L и модуля Ли M над L, M становится модулем Ли над L' посредством ограничения действия.
LaTeX
$$$$\text{If } M \text{ is a Lie } L\text{-module, then } M \text{ is a Lie } L'\text{-module with action restricted to } L'. $$$$
Lean4
/-- Given a Lie algebra `L` containing a Lie subalgebra `L' ⊆ L`, together with a Lie module `M` of
`L`, we may regard `M` as a Lie module of `L'` by restriction. -/
instance lieModule [LieModule R L M] : LieModule R L' M
where
smul_lie t x m := by rw [coe_bracket_of_module, Submodule.coe_smul_of_tower, smul_lie, coe_bracket_of_module]
lie_smul t x m := by simp only [coe_bracket_of_module, lie_smul]
