transcendental number

Stream: new members

[Mii Nguyen]

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]

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]

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

[Patrick Massot]

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

[Patrick Massot]

Computer scientists are so picky with naming conventions...

[Mii Nguyen]

@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]

You should also fix Mario's comment.

[Mii Nguyen]

thank you all!

[Kenny Lau]

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

[Floris van Doorn]

@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]

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.