mk' — Mathlib

English

There is a LieModuleHom structure on mk' N, giving a linear map from M to M/N that respects the Lie action.

Русский

Существует структура гомоморфизма LieModule на mk' N, задающая линейное отображение $M \\to M/N$, совместимое с действием Ли.

LaTeX

$$@[simp] def mk' : M →ₗ⁅R,L⁆ M ⧸ N$$

Lean4

/-- `LieSubmodule.Quotient.mk` as a `LieModuleHom`. -/
@[simps]
def mk' : M →ₗ⁅R,L⁆ M ⧸ N :=
  { N.toSubmodule.mkQ with
    toFun := mk
    map_lie' := fun {_ _} => rfl }

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