mathlib3 documentation

analysis.normed_space.star.matrix

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.