Zulip Chat Archive
Stream: new members
Topic: natural log and e
Callum Cassidy-Nolan (Feb 23 2022 at 05:12):
If this doesn't exist in mathlib, would it be ok if I add it ?
Junyan Xu (Feb 23 2022 at 05:31):
seems people are happy with real.exp 1
: https://leanprover-community.github.io/mathlib_docs/data/complex/exponential_bounds.html
Last updated: May 02 2025 at 03:31 UTC