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.

Estimated changes