Mathlib v3 is deprecated. Go to Mathlib v4

Theorem spectrum.exp_mem_exp

Modification history

2022-03-13 14:52
src/analysis/normed_space/spectrum.lean
feat(analysis/*/{exponential, spectrum}): spectrum of a selfadjoint element is real (#12417) …
Added spectrum.exp_mem_expView on Github →