Commit 2022-09-21 20:56 88f41bb0

View on Github →

feat(data/complex/exponential): positivity extension for real.exp (#16492) Add positivity_exp, a positivity extension to prove 0 < real.exp r for all r.

Estimated changes