PR #4301: feat(liouville_theorem): lemmas of Liouville th...

Stream: triage

[Random Issue Bot]

Today I chose PR 4301 for discussion!

feat(liouville_theorem): lemmas of Liouville theorem
Created by @Jujian Zhang (@jjaassoonn) on 2020-09-28
Labels: awaiting-review

Is this PR still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose PR 4301 for discussion!

feat(liouville_theorem): lemmas of Liouville theorem
Created by @Jujian Zhang (@jjaassoonn) on 2020-09-28
Labels: awaiting-review

Is this PR still relevant? Any recent updates? Anyone making progress?

[Kevin Buzzard]

I hope to find the time to look at this PR soon. Jujian was an MSc student of mine.

[Random Issue Bot]

Today I chose PR 4301 for discussion!

feat(liouville_theorem): lemmas of Liouville theorem
Created by @Jujian Zhang (@jjaassoonn) on 2020-09-28
Labels: WIP, awaiting-author

Is this PR still relevant? Any recent updates? Anyone making progress?

[Damiano Testa]

I still have one (or maybe two) PRs in this thread: there is the proof that Liouville number exist that is still missing in mathlib. I have an almost-ready-for-mathlib-review file on this, but I have not been able to get it through the system before I got swamped on other stuff! I plan to make further progress with this, within a couple of weeks.

[Damiano Testa]

Also, when I say "I", I really mean that my contribution has been to massage Jujian's files, to adapt them to mathlib!

[Ruben Van de Velde]

Does the work you've done include the proof that transcendental implies irrational?

[Damiano Testa]

If I remember correctly, transcendental => irrational is already there. There is certainly a proof that Liouville => transcendental, using Liouville => irrational. I cannot remember about the implication transcendental => irrational, but I assume that it is there!

[Damiano Testa]

I checked the file data/real/irrational.

Transcendental is defined as non-algebraic and I am pretty sure that rational => algebraic is there. So, "transcendental => irrational" may not be stated, but should not be hard!

[Damiano Testa]

There are certainly better proofs, but this works:

import data.real.irrational
import ring_theory.algebraic

open polynomial

lemma transcendental.irrational {r : ℝ} (tr : transcendental ℚ r) : irrational r :=
begin
  rintro ⟨a, rfl⟩,
  refine tr ⟨X - C a, X_sub_C_ne_zero a, _⟩,
  rw [alg_hom.map_sub, sub_eq_zero, aeval_X, aeval_C],
  refl,
end

[Damiano Testa]

I updated the name, so that it would work with dot.notation, I believe. If people think that this might be useful, I can PR it to mathlib.

[Damiano Testa]

PR #6721

I split the proof into two parts.

• is_algebraic_of_mem: if A is an R-algebra and r : R, then algebra_map R A r is algebraic over R.
• transcendental.irrational: the "contrapositive" of is_algebraic_of_mem, in the case of a transcendental $\mathbb{R}$ viewed as a $\mathbb{Q}$-algebra.

[Damiano Testa]

This is just to give visibility to a name-change: are people happy with the name of the lemma below? (Suggested by Eric)

/-- An element of `R` is algebraic, when viewed as an element of the `R`-algebra `A`. -/
lemma is_algebraic_algebra_map (a : R) : is_algebraic R (algebra_map R A a) :=
⟨X - C a, X_sub_C_ne_zero a, by simp only [aeval_C, aeval_X, alg_hom.map_sub, sub_self]⟩

[Johan Commelin]

LGTM