English
Conjugating a permutation by k translates its cycle-factor structure by k.
Русский
Сопряжение перестановки по k переносит её цикл-факторы соответствующим образом.
LaTeX
$$theorem cycleFactorsFinset_conj (g k : Perm α) : (ConjAct.toConjAct k • g).cycleFactorsFinset = Finset.map (MulAut.conj k).toEquiv.toEmbedding g.cycleFactorsFinset$$
Lean4
theorem cycleFactorsFinset_conj (g k : Perm α) :
(ConjAct.toConjAct k • g).cycleFactorsFinset =
Finset.map (MulAut.conj k).toEquiv.toEmbedding g.cycleFactorsFinset :=
by
ext c
rw [ConjAct.smul_def, ConjAct.ofConjAct_toConjAct, Finset.mem_map_equiv, ← mem_cycleFactorsFinset_conj g k]
-- We avoid `group` here to minimize imports while low in the hierarchy;
-- typically it would be better to invoke the tactic.
simp [mul_assoc]
