Algebra · existing Mathlib declaration

Burnside's Lemma

Let a finite group α act on β, and let Ω be the set of orbits. If every individual fixed-point set and Ω are finite, then adding the number of fixed points over all group elements gives |Ω| × |α|.

finite group actions
fixed points
orbit quotients
stabilizers
double counting
equivalences of finite types

The theorem at a glance

Burnside's Lemma at a glance

A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.

An ivory and dark-green poster states the three finiteness hypotheses, the exact fixed-point cardinality identity, and the equivalence between fixed incidences and orbit–group pairs. — The sum of fixed-set cardinalities equals the number of orbits multiplied by the group cardinality.

Formal orientation

Statement map

This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is authoritative.

Original pixels inspected. The distinct Scientific diagram clearly defines the fixed-incidence type I, displays I ≃ Ω × α, and gives the exact multiplication-form cardinality identity. Its illustrative marks balance exactly: 24 fixed incidences on the left and 4 × 6 orbit–group pairs on the right. It does not enclose all of β or introduce a division identity. — Fixed-point incidences and orbit–group pairs are two finite presentations of the same counted type.

Complementary intuition

A mathematical landmark

Burnside's lemma is a central bridge between symmetry and enumeration. Mathlib's proof exposes the underlying two-way count as an equivalence between the sigma type of fixed-point incidences and the product of the orbit quotient with the acting group.

The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.

Authoritative formal type

Exact Mathlib statement

theorem MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group {α : Type u} {β : Type v} [Group α] [MulAction α β] [Fintype α] [∀ a : α, Fintype <| MulAction.fixedBy β a] [Fintype (Quotient <| MulAction.orbitRel α β)] : (∑ a : α, Fintype.card (MulAction.fixedBy β a)) = Fintype.card (Quotient <| MulAction.orbitRel α β) * Fintype.card α

Selected evidence declaration text

theorem MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group {α : Type u} {β : Type v} [Group α] [MulAction α β] [Fintype α] [∀ a : α, Fintype <| MulAction.fixedBy β a] [Fintype (Quotient <| MulAction.orbitRel α β)] : (∑ a : α, Fintype.card (MulAction.fixedBy β a)) = Fintype.card (Quotient <| MulAction.orbitRel α β) * Fintype.card α

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed pageCurrent public presentation reviewed

Accepted Atlas resultNot recorded for the preferred artifact

These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.

Claim boundary

No new theorem is claimed

This target indexes Mathlib's multiplication-form Burnside lemma for a group α acting on β. It assumes Fintype α, a Fintype instance for each fixed-point subtype fixedBy β a, and a Fintype instance for the orbit quotient Ω; it concludes that the sum of the fixed-set cardinalities equals Fintype.card Ω multiplied by Fintype.card α.

The selected declaration does not require or provide a blanket Fintype β instance.
The selected declaration states a multiplication identity, not an average or division identity.
The equivalence used by the proof is noncomputable and does not select a canonical orbit representative.
Proof Atlas did not originate Burnside's lemma or Mathlib's declaration.
The generated explanation and visuals are not proof evidence.

Provenance

Origin and evidence stay separate

Existing declaration: MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group in mathlib
Relationship: The checked artifact is the upstream declaration itself
Preferred checked artifact: artifact.library.mathlib.burnside-lemma.v001
Source handling: Verified upstream reference; no mirrored source package