quot_mk_eq_mk

Mathlib.Algebra.Group.Conj

URI: https://scilib.ai/kg/mathlib#ConjClasses.quot_mk_eq_mk

English

Same content as above: the quotient image of a equals the conjugacy class of a.

Русский

Того же содержания формула: образ элемента a в фактор-множество равен классу сопряжённости a.

LaTeX

$$$\llbracket a \rrbracket = \mathrm{ConjClasses.mk}(a)$$$

Lean4

theorem quot_mk_eq_mk (a : α) : Quot.mk Setoid.r a = ConjClasses.mk a :=
  rfl

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

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

Разделы

Аффилиация

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