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} [IsROrC 𝕜] [Fintype n] [DecidableEq n] {U : Matrix n n 𝕜} (hU : U ∈ Matrix.unitaryGroup n 𝕜) (i : n) (j : n) : ‖U i j‖ ≤ 1

theorem entrywise_sup_norm_bound_of_unitary {𝕜 : Type u_1} {n : Type u_3} [IsROrC 𝕜] [Fintype n] [DecidableEq n] {U : Matrix n n 𝕜} (hU : U ∈ Matrix.unitaryGroup n 𝕜) : ‖U‖ ≤ 1

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