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

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