Commit 2024-09-11 15:20 ef7e491a

feat(GroupTheory/GroupAction/Quotient): equivSubgroupOrbitsQuotientGroup (#15506) Add the equivalence:

/-- Given a group acting freely and transitively, an equivalence between the orbits under the
action of a subgroup and the quotient group. -/
@[to_additive "Given an additive group acting freely and transitively, an equivalence between the
orbits under the action of an additive subgroup and the quotient group."]
noncomputable def equivSubgroupOrbitsQuotientGroup [IsPretransitive α β]
    (free : ∀ y : β, MulAction.stabilizer α y = ⊥) (H : Subgroup α) :
    orbitRel.Quotient H β ≃ α ⧸ H where

(note: this equivalence is parametrized by the variable (x : β) defined earlier in the file). From AperiodicMonotilesLean.