mem_orbit_iff

Mathlib.GroupTheory.GroupAction.Defs

URI: https://scilib.ai/kg/mathlib#MulAction.mem_orbit_iff

English

Symmetry of the conjugation action: the inverse action sends h to g^{-1} h g.

Русский

Симметрия сопряжения: обратное действие отправляет h в g^{-1} h g.

LaTeX

$$$↑((MulAut.conjNormal g).symm h) = g^{-1} h g$$$

Lean4

@[to_additive]
theorem mem_orbit_iff {a₁ a₂ : α} : a₂ ∈ orbit M a₁ ↔ ∃ x : M, x • a₁ = a₂ :=
  Iff.rfl

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

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

Разделы

Аффилиация

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