mathlib

50c30283 - chore(analysis/normed_space/operator_norm): move `continuous_linear_map.op_norm_lsmul` into the correct section (#13790)

chore(analysis/normed_space/operator_norm): move `continuous_linear_map.op_norm_lsmul` into the correct section (#13790) This was in the "seminorm" section but was about regular norms. Also relaxes some other typeclasses in the file. This file is still a mess with regards to assuming `nondiscrete_normed_field` when `normed_field` is enough, but that would require substantially more movement within the file. This cleans up after #13165 and #13538