Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-31 16:05 78f647f8

View on Github →

chore(order/filter, topology/algebra): golf (#18097)

Estimated changes

Modified src/order/filter/n_ary.lean

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

added theorem has_continuous_inv.of_nhds_one

deleted theorem topological_group.of_nhds_aux