cycleFactorsFinset_conj_eq — Mathlib

English

Conjugating a permutation by a transitive action yields the same cycle-factors structure up to the conjugation.

Русский

Сопряжение перестановки по эквивалентности сохраняет цикл-факторы, изменённые только конъюгацией.

LaTeX

$$theorem cycleFactorsFinset_conj_eq (k : ConjAct (Perm α)) (g : Perm α) : cycleFactorsFinset (k • g) = k • cycleFactorsFinset g$$

Lean4

theorem cycleFactorsFinset_conj_eq (k : ConjAct (Perm α)) (g : Perm α) :
    cycleFactorsFinset (k • g) = k • cycleFactorsFinset g :=
  by
  ext c
  rw [← mem_cycleFactorsFinset_conj' k⁻¹ (k • g) c]
  simp only [inv_smul_smul]
  exact Finset.inv_smul_mem_iff

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