normed_group_hom): remove bound_by (#7860)

Commit

4 years ago

chore(analysis/normed_space/normed_group_hom): remove bound_by (#7860) `bound_by f C` is the same as `∥f∥ ≤ C` and it is therefore useless now that we have `∥f∥`.

Author

riccardobrasca

Parents

0f8e79ea

mathlib 0a80efb3 - chore(analysis/normed_space/normed_group_hom): remove bound_by (#7860)

mathlib
0a80efb3 - chore(analysis/normed_space/normed_group_hom): remove bound_by (#7860)