Mathlib v3 is deprecated. Go to Mathlib v4

Theorem star_exp

Modification history

2022-05-08 18:01
src/analysis/normed_space/exponential.lean
feat(topology/algebra/infinite_sum): add `tsum_star` (#13999) …
Modified star_expView on Github →
2022-03-13 14:52
src/analysis/normed_space/exponential.lean
feat(analysis/*/{exponential, spectrum}): spectrum of a selfadjoint element is real (#12417) …
Added star_expView on Github →