sameCycle_conj — Mathlib

English

Conjugating a permutation by g preserves the SameCycle relation up to the relabeling x ↦ g⁻¹x, y ↦ g⁻¹y.

Русский

Приведение перестановки f к g f g⁻¹ сохраняет отношение той же самой цикла при замене перемещений x↦g⁻¹x, y↦g⁻¹y.

LaTeX

$$$\\forall f,g: \\mathrm{Perm}(\\alpha),\\; \\forall x,y:\\alpha,\\; \\mathrm{SameCycle}(g f g^{-1})\\ x\\ y \\iff \\mathrm{SameCycle}(f)\\ (g^{-1}x)\\ (g^{-1}y).$$$

Lean4

@[simp]
theorem sameCycle_conj : SameCycle (g * f * g⁻¹) x y ↔ SameCycle f (g⁻¹ x) (g⁻¹ y) :=
  exists_congr fun i => by simp [conj_zpow, eq_inv_iff_eq]

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