feat(*): `A ⧸ B` notation for quotients in algebra (#10501)
We introduce a class `has_quotient` that provides `⧸` (U+29F8 BIG SOLIDUS) notation for quotients, e.g. if `H : subgroup G` then `quotient_group.quotient H` is now written as `G ⧸ H`. Thanks to @jcommelin for suggesting the initial design.
Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Notation.20for.20group.28module.2Cideal.29.20quotients
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
