Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-27 11:20 b8627dba

View on Github →

refactor(topology/algebra/module/strong_topology): split of local convexity (#18671) The reason for this split is not only to reduce the import tree, but also to find a good home for proving with_seminorm versions of the local convexity results.

Estimated changes