mathlib3

daa257ff - feat(analysis/normed_space/star/basic): `matrix.entrywise_sup_norm_star_eq_norm` (#12201)

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. Co-authored-by: Hans Parshall <hparshall@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net>