Commit 2022-01-12 02:31 cdd44cd7
View on Github →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 :=