mem_orbit_conjAct — Mathlib

English

For all g,h in G, g lies in the orbit of h under ConjAct G iff g and h are conjugate.

Русский

Для любых g,h в G, элемент g лежит в орбите h под действием ConjAct G тогда и только тогда, когда g и h конъюгированы.

LaTeX

$$$g \in \operatorname{orbit}(\operatorname{ConjAct}(G), h) \iff \text{IsConj}(g,h)$$$

Lean4

@[simp]
theorem mem_orbit_conjAct {g h : G} : g ∈ orbit (ConjAct G) h ↔ IsConj g h := by
  rw [isConj_comm, isConj_iff, mem_orbit_iff]; rfl

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