Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebra_map_exp_comm_of_mem_ball

Modification history

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