Commit 2022-04-29 15:59 50c30283
View on Github →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