natural log and e

Stream: new members

[Callum Cassidy-Nolan]

If this doesn't exist in mathlib, would it be ok if I add it ?

[Junyan Xu]

seems people are happy with real.exp 1 : https://leanprover-community.github.io/mathlib_docs/data/complex/exponential_bounds.html