refactor(topology/algebra/uniform_group): Use `to_additive` (#11366)
refactor(topology/algebra/uniform_group): Use `to_additive` (#11366)

This PR replace the definition
`def topological_add_group.to_uniform_space : uniform_space G :=`
with the definition
`@[to_additive] def topological_group.to_uniform_space : uniform_space G :=`





leanprover-community/mathlib,leanprover-community/mathlib