[Merged by Bors] - feat(data/real/liouville, ring_theory/algebraic): a Liouville number is transcendental! #6204
Conversation
…rations for Liouville These lemmas are use to show that a Liouville number is transcendental. The statement that Liouville numbers are transcendental is the next PR in this sequence!
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
use Eric's suggestion
comments until some point
github-actions
bot
added
the
blocked-by-other-PR
adomani
changed the title
adomani
changed the title
adomani
added
the
awaiting-review
github-actions
bot
added
the
merge-conflict
github-actions
bot
removed
merge-conflict
|
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
…ommunity/mathlib into liouville_is_transcendental
src/data/real/liouville.lean
Outdated
| @@ -167,4 +166,44 @@ begin | |||
| exact (mem_roots fR0).mpr (is_root.def.mpr hy) } | |||
| end | |||
|
|
|||
| end irrational | |||
| theorem transcendental {x : ℝ} (liouville_x : liouville x) : | |||
| is_transcendental ℤ x :=begin | |||
There was a problem hiding this comment.
| is_transcendental ℤ x :=begin | |
| is_transcendental ℤ x := | |
| begin |
Also, it would be more satisfactory to have the statement that it is transcendental over the rationals. With your definitions, 1/2 is transcendental over the integers, but this is not of utmost interest...
There was a problem hiding this comment.
Oops, sorry, I misread the definition of transcendental. Still, why state it over integers over rationals?
There was a problem hiding this comment.
When I adopted this PR, I understood much less of Lean and I simply kept close to the existing statements. In particular, I did not question why there was a ℤ here instead of a ℚ.
In this specific case, the proof is structured so that it uses a polynomial with integer coefficients having an irrational root and derive an inequality from the fact that there are no denominators. I can write a separate step that a real (or complex!) number that is a root of a non-zero polynomial with rational coefficients is also the root of a non-zero polynomial with integer coefficients. This would likely go in a separate file, though.
I am happy to try this, if you think that it would be better!
There was a problem hiding this comment.
That's more of a math convention question. Typically, when I speak of algebraic or transcendental numbers this is over a field, not a ring. Over a ring, the relevant notion is rather to be an integer, and when I read "algebraic over R" as "root of a monic polynomial over R" (which is not the current definition in mathlib). But you're certainly more familiar with this area of mathematics than I am, so I'll leave it to you to decide.
There was a problem hiding this comment.
Until a few months ago, converting
- a monic polynomial with integer coefficients into a polynomial with rational coefficients or, the other way,
- a polynomial with integer coefficients into a monic polynomial with rational coefficients seemed to come at no cost!
For this reason, I never took much notice of "standard" conventions: I always took a mental note of whether an integer polynomial was monic or not, but often disregarded monicity assumptions about polynomials with coefficients in a field.
Lean has taught me otherwise. So, while I understand the differences, my view is now: this statement is a formalization of the correct mathematical principle and, for the moment, this is good enough for me!
I still think that the conversion between integer and rational coefficients for polynomials should be smoother, but this I would consider a different PR.
There was a problem hiding this comment.
ok. I don't mind on this PR, but I still think the definition of algebraic should be fixed at some point.
There was a problem hiding this comment.
I agree: I am playing right now with the conversion between polynomials with integer and rational coefficients!
There was a problem hiding this comment.
I think that it might take some time to get this into a workable tool. I could leave a comment saying that the is_algebraic and is_transcendental definitions need to interact better with fields of fractions, but at the moment, the API in this area does not make it easy, at least for me, to work with these notions.
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…ommunity/mathlib into liouville_is_transcendental
|
bors r+ |
github-actions
bot
added
ready-to-merge
…is transcendental! (#6204) This is an annotated proof. It finishes the first half of the Liouville PR. A taste of what is to come in a future PR: a proof that Liouville numbers actually exist! Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>
|
Sébastien, thank you for merging this and for all your reviews! |
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
…is transcendental! (#6204) This is an annotated proof. It finishes the first half of the Liouville PR. A taste of what is to come in a future PR: a proof that Liouville numbers actually exist! Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>
This is an annotated proof. It finishes the first half of the Liouville PR.
A taste of what is to come in a future PR: a proof that Liouville numbers actually exist!
Co-authored-by: Jujian Zhang jujian.zhang1998@outlook.com