mathlib documentation

analysis.normed_space.star.matrix

Unitary matrices #

This file collects facts about the unitary matrices over 𝕜 (either or ).

theorem entry_norm_bound_of_unitary {𝕜 : Type u_1} {n : Type u_3} [is_R_or_C 𝕜] [fintype n] [decidable_eq n] {U : matrix n n 𝕜} (hU : U matrix.unitary_group n 𝕜) (i j : n) :
U i j 1
theorem entrywise_sup_norm_bound_of_unitary {𝕜 : Type u_1} {n : Type u_3} [is_R_or_C 𝕜] [fintype n] [decidable_eq n] {U : matrix n n 𝕜} (hU : U matrix.unitary_group n 𝕜) :

The entrywise sup norm of a unitary matrix is at most 1.