## Stream: triage

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

#### Random Issue Bot (Nov 12 2020 at 14:17):

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 (Nov 27 2020 at 14:20):

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 (Nov 27 2020 at 14:31):

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

#### Random Issue Bot (Mar 16 2021 at 14:26):

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 (Mar 16 2021 at 14:47):

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 (Mar 16 2021 at 14:47):

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 (Mar 16 2021 at 15:03):

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

#### Damiano Testa (Mar 16 2021 at 15:05):

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 (Mar 16 2021 at 15:07):

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 (Mar 16 2021 at 15:45):

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 (Mar 16 2021 at 15:54):

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 (Mar 17 2021 at 05:50):

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 (Mar 17 2021 at 08:16):

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 (Mar 17 2021 at 08:17):

LGTM

Last updated: May 09 2021 at 15:11 UTC