Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-16 01:42 531db2ef

View on Github →

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

Estimated changes

Modified src/analysis/normed_space/compact_operator.lean

Modified src/topology/algebra/group.lean

Modified src/topology/algebra/infinite_sum.lean

Modified src/topology/algebra/module/finite_dimension.lean

Modified src/topology/algebra/nonarchimedean/adic_topology.lean

Modified src/topology/algebra/uniform_filter_basis.lean

Modified src/topology/algebra/uniform_group.lean

added theorem topological_comm_group_is_uniform

deleted theorem topological_group_is_uniform

added theorem topological_group_is_uniform_of_compact_space

Modified src/topology/algebra/valuation.lean

Modified src/topology/continuous_function/algebra.lean