mathlib3

49c4e8cb - generalize linear_map.bound_of_ball_bound'