exponential): `positivity` extension for `real.exp` (#16492)

Commit

3 years ago

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`.

Author

YaelDillies

Parents

b1539919

mathlib3 88f41bb0 - feat(data/complex/exponential): `positivity` extension for `real.exp` (#16492)

mathlib3
88f41bb0 - feat(data/complex/exponential): `positivity` extension for `real.exp` (#16492)