Zulip Chat Archive
Stream: new members
Topic: Euler's number
Huỳnh Trần Khanh (Jun 23 2021 at 08:07):
Do we have Euler's number in mathlib? Just wondering.
Kevin Buzzard (Jun 23 2021 at 08:14):
They don't even have "Euler's Number" in Wikipedia. What are you thinking of? If then search the docs for exponential and you'll find it.
Kevin Buzzard (Jun 23 2021 at 08:27):
(sorry for delay, apparently search on the API docs doesn't work on mobile?) Here are some numerical bounds: https://leanprover-community.github.io/mathlib_docs/data/complex/exponential_bounds.html and of course there are all the theorems about the exponential function too.
Eric Wieser (Jun 23 2021 at 12:00):
It's unfortunate that the pretty-printer does not roundtrip for things like #print 1.5 - those docs are awkward to read in doc-gen, yet the source code is clear
Kevin Buzzard (Jun 23 2021 at 16:12):
Oh I just assumed the rationals in lowest terms was just someone being nerdy :-)
Last updated: Dec 20 2023 at 11:08 UTC