New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(analysis/transcendental): e is transcendental #15954
Conversation
2k lines makes for a huge PR. I'd say anything above 300 is already large by mathlib standards. Is there any hope of splitting this off? |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is just a high-level review of the analysis/transcendental/deriv.lean
file. This could be moved to its own standalone PR. It should also be moved elsewhere, since none of those theorems have anything to do with transcendental numbers. I didn't review the proofs themselves nor attempted to golf them.
I also suggest you brand that file as proving results on the iterated derivative. I don't know if there's other files like that already (though I'd presume so).
|
||
theorem transcendental_iff_transcendental_over_ℚ (x : ℝ) : | ||
transcendental ℤ x ↔ transcendental ℚ x := | ||
iff.not $ is_fraction_ring.is_algebraic_iff ℤ ℚ ℝ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
iff.not $ is_fraction_ring.is_algebraic_iff ℤ ℚ ℝ | |
(is_fraction_ring.is_algebraic_iff ℤ ℚ ℝ).not |
Obsoleted by leanprover-community/mathlib4#6718 🎉 |
#3884, second attempt.