2022-10-24 21:05
src/analysis/normed_space/operator_norm.lean
feat(analysis/normed_space/operator_norm): characterize the operator norm over a `densely_normed_field` in terms of the supremum (#16963) …
Added continuous_linear_map.Sup_unit_ball_eq_nnnorm