mathlib3

1cbb31de - feat(analysis/normed_space/normed_group_hom): add lemmas (#7474)

feat(analysis/normed_space/normed_group_hom): add lemmas (#7474) From LTE. Written by @PatrickMassot - [x] depends on: #7459 Co-authored-by: Patrick Massot <patrickmassot@free.fr>