mem_stabilizer_iff — Mathlib

English

The cardinality of the set of six-permutations preserving a function equals a product of factorials of the fiber sizes.

Русский

Число элементов множества перестановок, сохраняющих функцию, равно произведению факториалов размеров волокон функции.

LaTeX

$$Set.card { g : Perm α | f ∘ g = f } = ∏ i, (Set.card { a : α | f a = i })!$$

Lean4

theorem mem_stabilizer_iff {g : (Perm α)ᵈᵐᵃ} : g ∈ stabilizer (Perm α)ᵈᵐᵃ f ↔ f ∘ (mk.symm g :) = f := by
  simp only [MulAction.mem_stabilizer_iff]; rfl

Похожие утверждения