mk

Mathlib.Algebra.GroupWithZero.Associated

URI: https://scilib.ai/kg/mathlib#Associates.mk

← MathLib Explorer

English

The canonical map sending an element to its associate class.

Русский

Единичная карта отправляет элемент в его класс ассоциированности.

LaTeX

$$$$\mathrm{Associates.mk}\, : M \to \mathrm{Associates}(M)$$$$

Lean4

/-- The canonical quotient map from a monoid `M` into the `Associates` of `M` -/
protected abbrev mk {M : Type*} [Monoid M] (a : M) : Associates M :=
  ⟦a⟧

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru