mathlib

cfc157d3 - chore(analysis/locally_convex/with_seminorms): change `with_seminorms` to a structure (#15388)

chore(analysis/locally_convex/with_seminorms): change `with_seminorms` to a structure (#15388) Change the class `with_seminorms` into a `structure`. The typeclass was useless in the first case since it can be only infered in trivial cases. Now it is somehow similar to how `has_basis` behaves.