mk — Mathlib · SciLib

English

The map mk sends an element of M to its coset in M/N, i.e., the canonical projection.

Русский

Отображение mk переводит элемент M в его косет в M/N, то есть каноническое проецирование.

LaTeX

$$$\\mathrm{mk}: M \\to M/N$$$

Lean4

/-- Map sending an element of `M` to the corresponding element of `M/N`, when `N` is a
lie_submodule of the lie_module `N`. -/
abbrev mk : M → M ⧸ N :=
  Submodule.Quotient.mk

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