mathlib

1c8ce7e0 - feat(data/complex): real exponential bounds (#14087)

feat(data/complex): real exponential bounds (#14087) Bounds on the real exponential function near 1, derived from the complex versions. Co-authored-by: Bhavik Mehta <bm489@cam.ac.uk>