mathlib

9a17b556 - feat(analysis/normed_space/basic): `norm_entry_le_entrywise_sup_norm` (#12159)

feat(analysis/normed_space/basic): `norm_entry_le_entrywise_sup_norm` (#12159) The entries of a matrix are at most the entrywise sup norm. Co-authored-by: Hans Parshall <hparshall@users.noreply.github.com>