Commit 2022-10-11 09:55 0fbd703b
View on Github →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.