mathlib

6e5e3f68 - feat(analysis/locally_convex): the topology of a locally convex space is generated by seminorms (#15035)

feat(analysis/locally_convex): the topology of a locally convex space is generated by seminorms (#15035) This PR provides the proof that every locally convex space has a family of seminorms that induces the topology. This PR also adds a new simp-lemma `is_R_or_C.real_norm`, which calculates the norm of a real number `r` coerced into a `is_R_or_C` type as the norm of `r`. This made it necessary to change some proofs in a few places. Co-authored-by: Moritz Doll <doll@uni-bremen.de>