mathlib3

79edde24 - feat(topology/discrete_quotient): Add a few lemmas about discrete quotients (#7454)

feat(topology/discrete_quotient): Add a few lemmas about discrete quotients (#7454) This PR adds the `discrete_quotient.map` construction and generally improves on the `discrete_quotient` API.