mathlib

c2a30bef - feat(analysis/normed_space/normed_group_hom): add norm_noninc.neg (#9658)