Theorems · Definition · group theory

AddAction.equivAddSubgroupOrbitsQuotientAddGroup

{G : Type u} →
  {X : Type v} →
    [inst : AddGroup G] →
      [inst_1 : AddAction G X] →
        X →
          [AddAction.IsPretransitive G X] →
            [IsCancelVAdd G X] → (H : AddSubgroup G) → AddAction.orbitRel.Quotient (↥H) X ≃ G ⧸ H

Given an additive group acting freely and transitively, an equivalence between the orbits under the action of an additive 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

AddGroupAddActionAddAction.IsPretransitiveIsCancelVAdd