Commit 2022-03-13 14:52 223e7428
View on Github →feat(analysis/*/{exponential, spectrum}): spectrum of a selfadjoint element is real (#12417)
This provides several properties of the exponential function and uses it to prove that for 𝕜 = ℝ
or 𝕜 = ℂ
, exp 𝕜 𝕜
maps the spectrum of a : A
(where A
is a 𝕜
-algebra) into the spectrum of exp 𝕜 A a
. In addition, exp ℂ A (I • a)
is unitary when a
is selfadjoint. Consequently, the spectrum of a selfadjoint element is real.