# Zulip Chat Archive

## Stream: new members

### Topic: transcendental number

#### Mii Nguyen (Apr 04 2019 at 08:59):

I try to make a definition of an algebraic number:

def is_algebraic_number{x: ℝ} := ∀ p:polynomial ℤ, ¬ is_root p x

But it expected that x and p are in the same semi-ring alpha. Here is what I found in the definition of ` is_root`

def is_root (p : polynomial α) (a : α) : Prop := p.eval a = 0

What should I do in this case? Thank you.

#### Patrick Massot (Apr 04 2019 at 09:17):

`def is_algebraic_number{x: ℝ} := ∀ p:polynomial ℤ, ¬ eval₂ int.cast x p = 0`

there may be a better looking solution, but this does what you want

#### Mario Carneiro (Apr 04 2019 at 09:18):

this looks like the definition of a transcendental number, not an algebraic number

#### Patrick Massot (Apr 04 2019 at 09:19):

I didn't look at the name, I fixed the definition...

#### Patrick Massot (Apr 04 2019 at 09:19):

Computer scientists are so picky with naming conventions...

#### Mii Nguyen (Apr 04 2019 at 09:33):

@Patrick Massot It lack an important condition that p is not zero polynomial.

I fixed it by

def is_transcendental_number{x: ℝ} := ∀ (p:polynomial ℤ) (p ≠ 0 ), ¬ is_root p x

and it works

#### Johan Commelin (Apr 04 2019 at 09:33):

You should also fix Mario's comment.

#### Mii Nguyen (Apr 04 2019 at 09:35):

thank you all!

#### Kenny Lau (Apr 04 2019 at 09:36):

of course this definition is still defective... the number should be an explicit argument

#### Floris van Doorn (Apr 05 2019 at 16:10):

@Mii Nguyen That last definition is not at all what you want. If you `#print`

it, you will see that what you defined is

def is_transcendental_number : Π {x : ℝ}, Prop := λ {x : ℝ}, polynomial ℤ → ∀ (p : polynomial ℝ), p ≠ 0 → ¬is_root p x

You want the following:

def is_transcendental_number (x : ℝ) : Prop := ∀(p : polynomial ℤ), p ≠ 0 → ¬ eval₂ int.cast x p = 0

If you want, you can abbreviate this to

def is_transcendental_number (x : ℝ) : Prop := ∀(p ≠ 0), ¬ eval₂ int.cast x p = 0

#### Floris van Doorn (Apr 05 2019 at 16:13):

The problem with your definition is that you didn't have a name to the hypothesis `(p ≠ 0)`

. You should write `(h : p ≠ 0)`

or `p ≠ 0 → ...`

. The syntax you used is notation for "for all `p`

not equal to `0`

" so this is a new `p`

different from the previous one.

Last updated: May 13 2021 at 20:13 UTC