mathlib

abdc3164 - feat(analysis/normed_space/normed_group_hom): add lemmas (#7875)