orbitRel_conjAct

Mathlib.GroupTheory.GroupAction.ConjAct

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

English

The orbit relation for ConjAct G coincides with the IsConj relation.

Русский

Отношение орбит ConjAct G совпадает с отношением IsConj.

LaTeX

$$$\text{orbitRel}(\operatorname{ConjAct} G, G) = \text{IsConj}$$$

Lean4

theorem orbitRel_conjAct : ⇑(orbitRel (ConjAct G) G) = IsConj :=
  funext₂ fun g h => by rw [orbitRel_apply, mem_orbit_conjAct]

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

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

Разделы

Аффилиация

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