Documentation
LeanOA
.
ForMathlib
.
Analysis
.
CStarAlgebra
.
Spectrum
Search
return to top
source
Imports
Init
Mathlib.Analysis.CStarAlgebra.Spectrum
Imported by
spectrum
.
norm_eq_one_of_unitary
source
theorem
spectrum
.
norm_eq_one_of_unitary
{
𝕜
:
Type
u_1}
[
NormedField
𝕜
]
{
E
:
Type
u_2}
[
NormedRing
E
]
[
StarRing
E
]
[
CStarRing
E
]
[
NormedAlgebra
𝕜
E
]
[
CompleteSpace
E
]
{
u
:
E
}
(
hu
:
u
∈
unitary
E
)
⦃
z
:
𝕜
⦄
(
hz
:
z
∈
spectrum
𝕜
u
)
:
‖
z
‖
=
1