Mathlib v3 is deprecated. Go to Mathlib v4

Theorem real.exp_eq_exp

Modification history

2020-12-09 04:36
src/data/complex/exponential.lean
feat(analysis/special_functions): `real.log` is infinitely smooth away from zero (#5116) …
Added real.exp_eq_expView on Github →