Theorems · Theorem · group theory

AddAction.sum_card_fixedBy_eq_card_orbits_mul_card_addGroup

∀ (G : Type u) (X : Type v) [inst : AddGroup G] [inst_1 : AddAction G X] [inst_2 : Fintype G]
  [inst_3 : (g : G) → Fintype ↑(AddAction.fixedBy X g)] [inst_4 : Fintype (Quotient (AddAction.orbitRel G X))],
  ∑ g, Fintype.card ↑(AddAction.fixedBy X g) = Fintype.card (Quotient (AddAction.orbitRel G X)) * Fintype.card G

Burnside's lemma : given a finite additive group G acting on a type X, the sum the orders of the stabilisers coincides with the number of orbits multiplied by the order of G. [Wikidata Q1330377](https://www.wikidata.org/wiki/Q1330377)

Defined in

Mathlib.GroupTheory.GroupAction.Quotient

Cited by

0 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupAddActionFintypeFintypeFintype