# 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.