mathlib

223e7428 - feat(analysis/*/{exponential, spectrum}): spectrum of a selfadjoint element is real (#12417)

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.