# Commit 2022-09-30 18:24 6e5e3f68

View on Github →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.