toConjAct

Mathlib.GroupTheory.GroupAction.ConjAct

URI: https://scilib.ai/kg/mathlib#ConjAct.toConjAct

English

There is a natural group isomorphism from G to ConjAct G given by sending g to conjugation by g.

Русский

Существует естественный груповой изоморфизм из G в ConjAct G, отправляющий g в сопряжение by g.

LaTeX

$$$G \cong ConjAct(G)$ via $g \mapsto \text{Conj}(g)$$$

Lean4

/-- Reinterpret `g : G` as an element of `ConjAct G`. -/
def toConjAct : G ≃* ConjAct G :=
  ofConjAct.symm

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

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

Разделы

Аффилиация

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