mk_eq_mk_iff_isConj — Mathlib

English

Two elements a and b have the same conjugacy class if and only if a is conjugate to b.

Русский

Два элемента a и b имеют одинаковый класс сопряжённости тогда и только тогда, когда a сопряжён с b.

LaTeX

$$$\mathrm{ConjClasses.mk}\;a = \mathrm{ConjClasses.mk}\;b \;\iff\; IsConj\;a\;b$$$

Lean4

theorem mk_eq_mk_iff_isConj {a b : α} : ConjClasses.mk a = ConjClasses.mk b ↔ IsConj a b :=
  Iff.intro Quotient.exact Quot.sound

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