Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-11 22:34 c2a30bef

View on Github →

feat(analysis/normed_space/normed_group_hom): add norm_noninc.neg (#9658) From LTE.

Estimated changes