Commit 2023-01-18 09:22 26703ef2

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.