Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-11 02:16 0a80efb3

View on Github →

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∥.

Estimated changes

modified theorem normed_group_hom.bound