mathlib

47b12e7f - chore(analysis/locally_convex/strong_topology): generalize to semilinear maps (#18679)

chore(analysis/locally_convex/strong_topology): generalize to semilinear maps (#18679) This is needed to show that the space of C-linear maps is locally convex. Also generalizes the ring from `real` to a general ordered semiring, since the proofs didn't need the `real`s. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>