English
If a,b,c are pairwise distinct, the product swap a b * swap a c is a three-cycle and lies in the closure of the three-cycles.
Русский
Если a,b,c различны, то произведение swap a b · swap a c является трёхцикл и лежит в замыкании трёхциклов.
LaTeX
$$swap a b * swap a c ∈ closure {σ : Perm α | IsThreeCycle σ}$$
Lean4
/-- The cardinality of the type of permutations preserving a function -/
theorem stabilizer_card [DecidableEq α] [DecidableEq ι] [Fintype ι] :
Fintype.card { g : Perm α // f ∘ g = f } = ∏ i, (Fintype.card { a // f a = i })! := by
-- rewriting via Nat.card because Fintype instance is not found
rw [← Nat.card_eq_fintype_card, Nat.card_congr (subtypeEquiv mk fun _ ↦ ?_), Nat.card_congr MulOpposite.opEquiv,
Nat.card_congr (DomMulAct.stabilizerMulEquiv f).toEquiv, Nat.card_pi]
· exact Finset.prod_congr rfl fun i _ ↦ by rw [Nat.card_eq_fintype_card, Fintype.card_perm]
· rfl
