mkEquiv — Mathlib

English

There is a bijection between a commutative group and its conjugacy classes, given by mk.

Русский

Существует биекция между коммутативной группой и её классами сопряжённости, заданная mk.

LaTeX

$$$\mathrm{mkEquiv}: \alpha \simeq \mathrm{ConjClasses}(\alpha)$$$

Lean4

/-- The bijection between a `CommGroup` and its `ConjClasses`. -/
def mkEquiv : α ≃ ConjClasses α :=
  ⟨ConjClasses.mk, Quotient.lift id fun (_ : α) _ => isConj_iff_eq.1, Quotient.lift_mk _ _,
    by
    rw [Function.RightInverse, Function.LeftInverse, forall_isConj]
    solve_by_elim⟩

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