refactor(analysis/normed_space/operator_norm): split (#18205)
The file `analysis/normed_space/operator_norm` is now nearly 2000 lines long, and it's a pretty heavy import since it now contains everything on the strong topologies, etc. This PR splits out 250 lines:
- some lemmas about infinite sums under continuous linear maps to a new file `topology/algebra/module/infinite_sum` (they were already stated for topological vector spaces, so definitely in the wrong location before)
- some constructors for continuous linear maps between normed spaces to a new file `analysis/normed_space/continuous_linear_map`, which is intended to be a more lightweight import
Later I hope to refactor some other files (e.g. `is_R_or_C`, `analysis/complex/basic`) to import only the new file `analysis/normed_space/continuous_linear_map`, not `analysis/normed_space/operator_norm`.
