mk — Mathlib · SciLib

English

There is a canonical map from the group α to the quotient α / s, sending each element to its coset.

Русский

Существуют канонические отображения α → α / s, отправляющее элемент на его косет.

LaTeX

$$mk : α → α / s$$

Lean4

/-- The canonical map from a group `α` to the quotient `α ⧸ s`. -/
@[to_additive (attr := coe) /-- The canonical map from an `AddGroup` `α` to the quotient `α ⧸ s`. -/
    ]
abbrev mk (a : α) : α ⧸ s :=
  Quotient.mk'' a

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