Theorems · Definition · group theory

MulAction.equivSubgroupOrbitsQuotientGroup

{G : Type u} →
  {X : Type v} →
    [inst : Group G] →
      [inst_1 : MulAction G X] →
        X →
          [MulAction.IsPretransitive G X] →
            [IsCancelSMul G X] → (H : Subgroup G) → MulAction.orbitRel.Quotient (↥H) X ≃ G ⧸ H

Given a group acting freely and transitively, an equivalence between the orbits under the action of a subgroup and the quotient of the group by the subgroup.

Defined in

Mathlib.GroupTheory.GroupAction.Quotient

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupMulActionMulAction.IsPretransitiveIsCancelSMul