Zulip Chat Archive

Stream: new members

Topic: transcendental number


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 04 2019 at 09:18):

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

view this post on Zulip Patrick Massot (Apr 04 2019 at 09:19):

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

view this post on Zulip Patrick Massot (Apr 04 2019 at 09:19):

Computer scientists are so picky with naming conventions...

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 04 2019 at 09:33):

You should also fix Mario's comment.

view this post on Zulip Mii Nguyen (Apr 04 2019 at 09:35):

thank you all!

view this post on Zulip Kenny Lau (Apr 04 2019 at 09:36):

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

view this post on Zulip 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

view this post on Zulip 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