Commit 2022-03-13 07:59 daa257ff
View on Github →feat(analysis/normed_space/star/basic): matrix.entrywise_sup_norm_star_eq_norm (#12201)
This is precisely the statement needed for a normed_star_monoid
instance on matrices using the entrywise sup norm.