# Zulip Chat Archive

## 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