mathlib

e46daa0a - feat(analysis/normed_space/operator_norm): remove to_span_singleton_norm (#16654)

feat(analysis/normed_space/operator_norm): remove to_span_singleton_norm (#16654) Remove `continuous_linear_map.to_span_singleton_norm`. It is a duplicate of `continuous_linear_map.norm_to_span_singleton` (which has more explicit arguments and weaker type-class assumptions).