Mathlib v3 is deprecated. Go to Mathlib v4

Theorem commute.exp_unitary_add

Modification history

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