mathlib

ab2c546d - feat(data/quot): define `quotient.map` and `quotient.map₂` (dep: 1441) (#1442)

feat(data/quot): define `quotient.map` and `quotient.map₂` (dep: 1441) (#1442) * chore(algebra/group,logic/relator): review some explicit/implicit arguments * ring_hom.ext too * feat(data/quot): define `quotient.map` and `quotient.map₂` * Add comments * Fix a typo Co-Authored-By: Johan Commelin <johan@commelin.net>