mathlib
47dcecd2 - feat(data/complex/exponential): bounds on exp (#4432)

Commit
5 years ago
feat(data/complex/exponential): bounds on exp (#4432) Define `real.exp_bound` using `complex.exp_bound`. Deduce numerical bounds on `exp 1` analogous to those we have for pi. Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>
Author
Parents
Loading