mathlib

70772422 - doc (analysis/normed_space/operator_norm): cleanup (#1906)

doc (analysis/normed_space/operator_norm): cleanup (#1906) * doc (analysis/normed_space/operator_norm): cleanup * typo Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>