mathlib3

doc (analysis/normed_space/operator_norm): cleanup

#1906

Merged