Commit 2020-12-23 22:08 ceae5296
View on Github →chore(group_theory/coset): Make quotient_group.mk an abbreviation (#5377)
This allows simp lemmas about quotient.mk' to apply here, which currently do not apply.
The definition doesn't seem interesting enough to be semireducible.