Commit 2024-06-06 21:05 57c40988

feat(GroupTheory/GroupAction/Basic): various orbit / quotient lemmas (#11912) Add various lemmas about orbitRel.Quotient, mostly concerning orbitRel.Quotient.orbit, many concerning orbits for the action of a subgroup. Along with the lemmas there are instances

instance (x : orbitRel.Quotient G α) : MulAction G x.orbit where

and

instance (x : orbitRel.Quotient G α) : IsPretransitive G x.orbit where

both of which already have analogues for MulAction.orbit as opposed to orbitRel.Quotient.orbit - and lemmas about the above action on an orbit. From AperiodicMonotilesLean.