val_centralizer_smul — Mathlib

English

If k lies in the centralizer of {g} and c is a cycle-factor of g, then the action of k on c is simply conjugation, i.e., the underlying permutation is k c k^{-1}.

Русский

Если k лежит в центральизаторе {g} и c — цикл‑фактор g, то действия k на c есть простое сопряжение: k c k^{-1}.

LaTeX

$$$k \in \operatorname{Cent}({g}) \Rightarrow (k \cdot c : \text{Perm }\alpha) = k c k^{-1}$$$

Lean4

@[simp]
theorem val_centralizer_smul (k : Subgroup.centralizer { g }) (c : g.cycleFactorsFinset) :
    ((k • c :) : Perm α) = k * c * k⁻¹ :=
  rfl

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