Commit 2022-04-21 11:02 21bbe900
View on Github →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.