mathlib3

21bbe900 - feat(analysis/normed): more lemmas about the sup norm on pi types and matrices (#13536)

feat(analysis/normed): more lemmas about the sup norm on pi types and matrices (#13536) For now we name the matrix lemmas as `matrix.norm_*` and `matrix.nnnorm_*` to match `matrix.norm_le_iff` and `matrix.nnnorm_le_iff`. We should consider renaming these in future to indicate which norm they refer to, but should probably deal with agreeing on a name in a separate PR.