English
Let g be a finite permutation of α and k a member of the centralizer of {g}. For any cycle-factor c in the cycle-factors Finset of g, the action of k on c is conjugation, i.e. k · c equals the pair consisting of k c k^{-1} together with the fact that this lies in the appropriate cycle-factors Finset’s centralizer conjugation action.
Русский
Пусть g — конечная перестановка на множестве α, а k принадлежит центральизатору множества {g}. Для любого элемента‑цикла c в Finset factorCycle(g) действует сопряжение: k ⋅ c = ⟨k c k^{-1}, доказательство, что это сохраняется в фактор-факторов цикла ⟩.
LaTeX
$$$k \in \operatorname{Cent}({g}) \quad\text{и}\quad c \in g.cycleFactorsFinset\quad\Longrightarrow\quad k \cdot c = \langle k c k^{-1}, \operatorname{Subgroup.Centralizer.toConjAct_smul_mem_cycleFactorsFinset k. prop\, c.prop} \rangle$$$
Lean4
theorem centralizer_smul_def (k : centralizer { g }) (c : g.cycleFactorsFinset) :
k • c = ⟨k * c * k⁻¹, Subgroup.Centralizer.toConjAct_smul_mem_cycleFactorsFinset k.prop c.prop⟩ :=
rfl
