mk — Mathlib · SciLib

English

The canonical quotient map sends an element a ∈ α to its conjugacy class in ConjClasses α.

Русский

Каноническое отображение к фактор-множество отправляет элемент a ∈ α в его класс сопряжённости в ConjClasses α.

LaTeX

$$$\mathrm{ConjClasses.mk}\;:\alpha \to \mathrm{ConjClasses}(\alpha)$ is the canonical quotient map; i.e., sends a to its conjugacy class.$$

Lean4

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

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