Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes