ConjClasses — Mathlib

English

The quotient type ConjClasses α collects all conjugacy classes of a monoid α; it identifies elements that are conjugate.

Русский

Число конъюгаций ConjClasses α собирает все классы сопряжённости моноида α; он отождествляет элементы, которые сопряжены.

LaTeX

$$$\text{ConjClasses}(\alpha) = \text{Quotient}(IsConj.setoid\alpha)$$$

Lean4

/-- The quotient type of conjugacy classes of a group. -/
def ConjClasses (α : Type*) [Monoid α] : Type _ :=
  Quotient (IsConj.setoid α)

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