chore(analysis/normed_space/star/basic): split (#18194)
The import `analysis/normed_space/operator_norm` was added to this file by @j-loreaux in #16964, but nowadays `operator_norm` is quite a heavy import (it contains everything on the strong topologies, etc), whereas I hope that `normed_space/star/basic` can become a fairly lightweight one (because it is imported by `is_R_or_C` which is imported everywhere). I propose to split out the material from #16964.
