English
The natural cardinality of the image theorems matches the product of cycle-type factorial contributions.
Русский
Натуральная размерность образа совпадает с произведением факториалов вклада цикла типа.
LaTeX
$$nat_card_range_toPermHom$$
Lean4
theorem card_isConj_mul_eq :
Nat.card {h : Perm α | IsConj g h} *
((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
(∏ n ∈ g.cycleType.toFinset, (g.cycleType.count n)!)) =
(Fintype.card α)! :=
by
classical
rw [Nat.card_eq_fintype_card, ← nat_card_centralizer g]
rw [Subgroup.nat_card_centralizer_nat_card_stabilizer, Nat.card_eq_fintype_card]
convert MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct (Perm α)) g
· ext h
simp only [Set.mem_setOf_eq, ConjAct.mem_orbit_conjAct, isConj_comm]
· rw [ConjAct.card, Fintype.card_perm]
