# Commit 2023-01-18 09:22 26703ef2

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

.