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

Commit
3 years ago
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 :=`
Author
Parents
Loading