Commit 2022-03-13 14:52 223e7428

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.