Commit 2021-07-17 13:14 bd56531b
View on Github →chore(analysis/normed_space/operator_norm): use norm_one_class
(#8346)
- turn
continuous_linear_map.norm_id
into asimp
lemma; - drop its particular case
continuous_linear_map.norm_id_field
; - replace
continuous_linear_map.norm_id_field'
with anorm_one_class
instance.