Skip to content
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 #3884

Closed
wants to merge 4 commits into from

Conversation

jjaassoonn
Copy link
Collaborator


This branch contains some basic theorems about transcendental numbers. The code are not very idomatic, so helpsa re more than welcome.

Copy link
Collaborator

@jamesa9283 jamesa9283 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Some docstrings and a module docstrings here would be nice. If you are unsure of what I mean, look in some other files in mathlib. I believe that data/padics/padic_numbers.lean is a good example. Also it should probably be mentioned that docstrings are indicated using /-- *text* -/ for def, lemma, theorem etc and module docstrings are indicated using /-! *text* -/ and can have markdown formatting in them.

move irrational' definition to small_lemmas file
@PatrickMassot
Copy link
Member

Some docstrings and a module docstrings here would be nice. If you are unsure of what I mean, look in some other files in mathlib. I believe that data/padics/padic_numbers.lean is a good example. Also it should probably be mentioned that docstrings are indicated using /-- *text* -/ for def, lemma, theorem etc and module docstrings are indicated using /-! *text* -/ and can have markdown formatting in them.

See also https://leanprover-community.github.io/contribute/doc.html, and https://leanprover-community.github.io/contribute/index.html in general.

@jcommelin jcommelin added help-wanted The author needs attention to resolve issues WIP Work in progress labels Aug 20, 2020
@bryangingechen bryangingechen changed the title transcendental_things feat(analysis/transcendental): e is transcendental Aug 21, 2020
@bryangingechen
Copy link
Collaborator

This is a pretty big PR. Can you split off any smaller PRs? For instance, I think small_lemmas.lean could potentially be a PR on its own (though those lemmas may have to go to different parts of mathlib), and the material on Liouville numbers could also be a separate PR as well.

You can leave this one open and mark it "blocked-by-other-PR" with references to the other PRs until those get merged.

@bryangingechen bryangingechen added the awaiting-author A reviewer has asked the author a question or requested changes label Aug 22, 2020
@jjaassoonn jjaassoonn closed this Sep 17, 2020
@jjaassoonn
Copy link
Collaborator Author

I will split into smaller ones

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-author A reviewer has asked the author a question or requested changes help-wanted The author needs attention to resolve issues WIP Work in progress
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

5 participants