coeSubmodule — Mathlib

English

There is a canonical coercion from LieSubmodule to Submodule, identifying N with its carrier as a submodule of M.

Русский

Существует каноническое преобразование из LieSubmodule в Submodule, отождествляющее N с его носителем как подмодуль M.

LaTeX

$$$\\text{LieSubmodule}.\\text{coeSubmodule}: (N : \\text{Submodule} \\ M) \\text{ is the carrier of } N$$$

Lean4

instance (priority := mid) coeSubmodule : CoeOut (LieSubmodule R L M) (Submodule R M) :=
  ⟨toSubmodule⟩

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