Commit 2022-10-24 21:05 b06d2285

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.