uniform_group): add instance `topological_group_is_uniform_of_compact_space` (#16027)

Commit

3 years ago

feat(topology/algebra/uniform_group): add instance `topological_group_is_uniform_of_compact_space` (#16027) Also update doc string for `topological_group.to_uniform_space`. cc @ADedecker

Author

ocfnash

Parents

07d11baa

mathlib 531db2ef - feat(topology/algebra/uniform_group): add instance `topological_group_is_uniform_of_compact_space` (#16027)

mathlib
531db2ef - feat(topology/algebra/uniform_group): add instance `topological_group_is_uniform_of_compact_space` (#16027)