transcendence of $$e$$

Stream: maths

[Jujian Zhang]

Hi, everyone. I proved $\sum_{i=0}^\infty\frac{1}{10^{i!}}$ and transcendence of $e$.
Here is the repo.
https://github.com/jjaassoonn/transcendental

[Johan Commelin]

Fantastic!

[Kenny Lau]

Everything not PR'ed into mathlib is lost. -- Ancient Chinese Proverb

[Scott Morrison]

Let us know if you want advice about how to carve it up into mathlib-ready chunk!

[Heather Macbeth]

(wrong thread)

[Kevin Buzzard]

The proof relies on the fundamental theorem of calculus, a version of which is assumed as an axiom.

[Johan Commelin]

It would be really cool if we could formalise Tent–Ziegler, Computable functions of reals.

[Aaron Anderson]

I didn't know there was another Tent-Ziegler project, I only knew their model theory book...