Mathlib v3 is deprecated. Go to Mathlib v4

Def topological_group.to_uniform_space

Modification history

2022-01-12 02:31
src/topology/algebra/uniform_group.lean
refactor(topology/algebra/uniform_group): Use `to_additive` (#11366) …
Added topological_group.to_uniform_spaceView on Github →