Commit 2021-12-30 16:51 682f1e63
View on Github →feat(analysis/normed_space/operator_norm): generalize linear_map.bound_of_ball_bound (#11140)
This was proved over is_R_or_C but holds (in a slightly different form) over all nondiscrete normed fields.