Mathlib v3 is deprecated. Go to Mathlib v4

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 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.

Estimated changes