English
If G acts on X and both G and the set of orbits X/G are finite, then the sum of the sizes of fixed-point sets equals the product of the sizes, i.e., ∑_{g∈G} |Fix(g)| = |X/G| · |G|.
Русский
При конечной группе G, действующей на X, и конечном наборе орбит X/G; сумма количества фиксированных точек по g равна произведению числа орбит на размер группы.
LaTeX
$$sum_{g ∈ α} card(fixedBy β g) = card(Ω) · card(α)$$
Lean4
/-- **Burnside's lemma** : given a finite group `G` acting on a set `X`, the average number of
elements fixed by each `g ∈ G` is the number of orbits. -/
@[to_additive AddAction.sum_card_fixedBy_eq_card_orbits_mul_card_addGroup /--
**Burnside's lemma** : given a finite additive group `G` acting on a set `X`,
the average number of elements fixed by each `g ∈ G` is the number of orbits. -/
]
theorem sum_card_fixedBy_eq_card_orbits_mul_card_group [Fintype α] [∀ a : α, Fintype <| fixedBy β a] [Fintype Ω] :
(∑ a : α, Fintype.card (fixedBy β a)) = Fintype.card Ω * Fintype.card α := by
rw [← Fintype.card_prod, ← Fintype.card_sigma, Fintype.card_congr (sigmaFixedByEquivOrbitsProdGroup α β)]
