mathlib3

b8627dba - refactor(topology/algebra/module/strong_topology): split of local convexity (#18671)

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.