mathlib3

021baaee - feat(analysis/normed_space/linear_isometry): coercion injectivity lemmas and add_monoid_hom_class (#11434)

feat(analysis/normed_space/linear_isometry): coercion injectivity lemmas and add_monoid_hom_class (#11434) This also registers `linear_isometry` and `linear_isometry_equiv` with `add_monoid_hom_class`. I found myself wanting one of these while squeezing a simp, so may as well have all of them now.