instGroup

Mathlib.GroupTheory.GroupAction.ConjAct

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

English

The conjugation action on G forms a group isomorphic to G, i.e., ConjAct G carries the same group structure as G.

Русский

Действие сопряжения на G образует группу, изоморфную G; ConjAct G имеет такую же группу структуру, как G.

LaTeX

$$$\text{ConjAct}(G) \cong G$$$

Lean4

instance [Group G] : Group (ConjAct G) :=
  ‹Group G›

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

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

Разделы

Аффилиация

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