mathlib3

682f1e63 - feat(analysis/normed_space/operator_norm): generalize linear_map.bound_of_ball_bound (#11140)

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. Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>