Theorem uniformity_eq_comap_nhds_zero'

refactor(topology/algebra/uniform_group): Use `to_additive`. (#11662) …

style(*): use notation `𝓝` for `nhds` (#1582) …

chore(topology/*): @uniformity α _ becomes 𝓤 α (#814) …

feat(topology): split uniform_space and topological_structure

feat(analysis/topology/topological_groups): construct topologies out of a group and a neighbourhood filter at 0