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) :
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.