Commit 2022-05-17 17:18 ae6f59d7

feat(analysis/locally_convex/with_seminorms): pull back with_seminorms along a linear inducing (#13549) This show that, if f : E -> F is linear and the topology on F is induced by a family of seminorms p, then the topology induced on E through f is induced by the seminorms (p i) ∘ f.

• depends on: #13547