Theorems · Definition · group theory

MulAction.selfEquivSigmaOrbits

(G : Type u_1) →
  (α : Type u_2) →
    [inst : Group G] →
      [inst_1 : MulAction G α] → α ≃ (ω : MulAction.orbitRel.Quotient G α) × ↑(MulAction.orbit G (Quotient.out ω))

Decomposition of a type X as a disjoint union of its orbits under a group action.

Defined in

Mathlib.GroupTheory.GroupAction.Defs

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupMulAction