Unitary matrices #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.