mathlib

e25cbe0d - feat(category_theory/quotient): the quotient functor is full and essentially surjective (#7465)

feat(category_theory/quotient): the quotient functor is full and essentially surjective (#7465) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>