mathlib3

45d235e8 - feat(analysis/normed_space/star/matrix): `entrywise_sup_norm_bound_of_unitary` (#12255)

feat(analysis/normed_space/star/matrix): `entrywise_sup_norm_bound_of_unitary` (#12255) The entrywise sup norm of a unitary matrix is at most 1. I suspect there is a simpler proof! Co-authored-by: Hans Parshall <hparshall@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>