Commit 2023-01-17 20:29 3249a849

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.