Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-25 18:28 717c0732

View on Github →

refactor(topology/algebra/group): split file (#17697)

Estimated changes

Modified src/dynamics/flow.lean

Modified src/measure_theory/integral/riesz_markov_kakutani.lean

Modified src/measure_theory/measure/haar.lean

Modified src/topology/algebra/affine.lean

Renamed src/topology/algebra/group.lean to src/topology/algebra/group/basic.lean

deleted theorem topological_space.positive_compacts.locally_compact_space_of_group

Created src/topology/algebra/group/compact.lean

added theorem topological_space.positive_compacts.locally_compact_space_of_group

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

Modified src/topology/algebra/order/basic.lean

Modified src/topology/algebra/ring.lean

Modified src/topology/algebra/uniform_group.lean

Modified src/topology/metric_space/baire.lean

Modified src/topology/path_connected.lean