mathlib

ceae5296 - chore(group_theory/coset): Make `quotient_group.mk` an abbreviation (#5377)

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.