mathlib

0fbd703b - feat(topology/instances/add_circle): the additive circle `ℝ / (a ∙ ℤ)` is normal (T4) and second-countable (#16594)

feat(topology/instances/add_circle): the additive circle `ℝ / (a ∙ ℤ)` is normal (T4) and second-countable (#16594) The T4 fact is in mathlib already, via the `normed_add_comm_group` instance on `ℝ / (a ∙ ℤ)`, but this gives it earlier in the hierarchy. Co-authored-by: Alex Kontorovich <58564076+AlexKontorovich@users.noreply.github.com>