Commit 2023-02-02 05:17 cc9e72df

feat: port GroupTheory.QuotientGroup (#1996) porting notes:

1. near line 595: Lean 4 couldn't find a Setoid instance that Lean 3 found automatically (in part via unification).
2. near line 654, declaration quotientQuotientEquivQuotient: The ext calls were totally borked, and in the first case even manually applying the ext lemmas didn't work out of the box because Lean couldn't unify the types (this was egregious)