incl — Mathlib

English

If N ≤ N', the inclusion N → N' is a morphism of Lie modules.

Русский

Если N ⊆ N', включение N → N' является гомоморфизмом Ли-модулей.

LaTeX

$$If N \\le N', then inclusion : N →ₗ⁅R,L⁆ N' is a LieModuleHom$$

Lean4

/-- The inclusion of a Lie submodule into its ambient space is a morphism of Lie modules. -/
def incl : N →ₗ⁅R,L⁆ M :=
  { Submodule.subtype (N : Submodule R M) with map_lie' := fun {_ _} ↦ rfl }

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