English
KerParam induces an injection into the centralizer, reflecting the injectivity result for kerParam.
Русский
KerParam индуцирует инъекцию в центр, отражая результат инъективности kerParam.
LaTeX
$$kerParam_injective (g) : Function.Injective (kerParam g)$$
Lean4
theorem kerParam_range_card (g : Equiv.Perm α) :
Fintype.card (kerParam g).range = (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod :=
by
rw [Fintype.card_coeSort_range (kerParam_injective g)]
rw [Fintype.card_prod, Fintype.card_perm, Fintype.card_pi, card_fixedPoints]
apply congr_arg
rw [Finset.univ_eq_attach, g.cycleFactorsFinset.prod_attach (fun i ↦ Fintype.card (zpowers i)), cycleType,
Finset.prod_map_val]
refine Finset.prod_congr rfl (fun x hx ↦ ?_)
rw [Fintype.card_zpowers, (mem_cycleFactorsFinset_iff.mp hx).1.orderOf, Function.comp_apply]
