English
There is a natural MulAction of the centralizer of g on the finite set of g.cycleFactorsFinset given by conjugation; the action respects identity and multiplication.
Русский
Существует естественное действие умножения центральизатора на конечное множество cycleFactorsFinset, задаваемое сопряжением; действие сохраняет единицу и умножение.
LaTeX
$$cycleFactorsFinset_mulAction : MulAction (centralizer { g }) (g.cycleFactorsFinset)$$
Lean4
/-- The action by conjugation of `Subgroup.centralizer {g}`
on the cycles of a given permutation -/
def cycleFactorsFinset_mulAction : MulAction (centralizer { g }) g.cycleFactorsFinset
where
smul k
c :=
⟨ConjAct.toConjAct (k : Perm α) • c.val, Subgroup.Centralizer.toConjAct_smul_mem_cycleFactorsFinset k.prop c.prop⟩
one_smul
c := by
rw [← Subtype.coe_inj]
change ConjAct.toConjAct (1 : Perm α) • c.val = c
simp only [map_one, one_smul]
mul_smul k l
c := by
simp only [← Subtype.coe_inj]
change
ConjAct.toConjAct (k * l : Perm α) • c.val =
ConjAct.toConjAct (k : Perm α) • (ConjAct.toConjAct (l : Perm α)) • c.val
simp only [map_mul, mul_smul]
