incl' — Mathlib

English

The inclusion map incl' embeds L' into L as a Lie modules morphism, i.e., it is a LieModuleHom from L' (as a submodule) to L.

Русский

Включение incl' внедряет L' в L как морфизм модулей Ли.

LaTeX

$$$$\text{incl}' : L' \to_{\mathfrak{L}} L,$$$$

Lean4

/-- The embedding of a Lie subalgebra into the ambient space as a morphism of Lie modules. -/
def incl' : L' →ₗ⁅R,L'⁆ L :=
  { (L' : Submodule R L).subtype with map_lie' := rfl }

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