mathlib3

bd56531b - chore(analysis/normed_space/operator_norm): use `norm_one_class` (#8346)

chore(analysis/normed_space/operator_norm): use `norm_one_class` (#8346) * turn `continuous_linear_map.norm_id` into a `simp` lemma; * drop its particular case `continuous_linear_map.norm_id_field`; * replace `continuous_linear_map.norm_id_field'` with a `norm_one_class` instance.