Theorems · Definition · group theory

AddAction.sigmaFixedByEquivOrbitsProdAddGroup

(G : Type u) →
  (X : Type v) →
    [inst : AddGroup G] →
      [inst_1 : AddAction G X] → (g : G) × ↑(AddAction.fixedBy X g) ≃ Quotient (AddAction.orbitRel G X) × G

Burnside's lemma : a (noncomputable) bijection between the disjoint union of all {x ∈ X | g • x = x} for g ∈ G and the product G × Ω, where G is an additive group acting on X and Ω = X/G denotes the quotient of X by the relation orbitRel G X.

Defined in

Mathlib.GroupTheory.GroupAction.Quotient

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddGroupAddAction