mathlib3

b06d2285 - feat(analysis/normed_space/operator_norm): characterize the operator norm over a `densely_normed_field` in terms of the supremum (#16963)

feat(analysis/normed_space/operator_norm): characterize the operator norm over a `densely_normed_field` in terms of the supremum (#16963) This provides a few results pertaining to the operator norm over a `densely_normed_field`. In particular, if `0 ≤ r < ∥f∥` then there exists some `x` with `∥x∥ ≤ 1` such that `r < ∥f x∥`. Consequently, the operator norm is the supremum of the norm of the image of the unit ball under `f`.