mathlib

3d999265 - feat(analysis/normed/group/SemiNormedGroup): add iso_isometry_of_norm_noninc (#9710)