English
Under suitable finiteness hypotheses, the cardinality of the stabilizer of f under Perm α equals the product over i of factorials of fiber sizes.
Русский
При подходящих ограничениях на размер, кардинал стабилизатора функции f под Perm α равен произведению факториалов размеров волокон функции.
LaTeX
$$Fintype.card { g : Perm α // f ∘ g = f } = ∏ i, (Fintype.card { a // f a = i })!$$
Lean4
/-- The cardinality of the set of permutations preserving a function -/
theorem stabilizer_ncard [Finite α] [Fintype ι] :
Set.ncard {g : Perm α | f ∘ g = f} = ∏ i, (Set.ncard {a | f a = i})! := by
classical
cases nonempty_fintype α
simp only [← Nat.card_coe_set_eq, Set.coe_setOf, card_eq_fintype_card]
exact stabilizer_card f
