Zulip Chat Archive

Stream: new members

Topic: cubic equation


view this post on Zulip Mii Nguyen (Apr 16 2019 at 04:12):

I try to definite a cubic equation as a polynomial function .
My first test start with

open polynomial
variable X: polynomial 
def test (a: ):polynomial  := C a * X

The problem here is that I can't use the indeterminant Xavailable in the module polynomial.lean and that it don't accept C a*X as a polynomial. Would someone help me with this? Thank you.

view this post on Zulip Mario Carneiro (Apr 16 2019 at 04:23):

You will need to open polynomial to write just C and X as opposed to polynomial.C and polynomial.X. You don't want variable X because then you are making X refer to an arbitrary polynomial rather than the indeterminate

view this post on Zulip Mii Nguyen (Apr 16 2019 at 04:26):

@Mario Carneiro I already did this in my test

view this post on Zulip Johan Commelin (Apr 16 2019 at 04:26):

Do you have open polynomial in your file?

view this post on Zulip Mario Carneiro (Apr 16 2019 at 04:26):

I mean

open polynomial
def test (a: ):polynomial  := C a * X

view this post on Zulip Mii Nguyen (Apr 16 2019 at 04:26):

yes, this is my test

view this post on Zulip Mario Carneiro (Apr 16 2019 at 04:27):

no variable line

view this post on Zulip Mario Carneiro (Apr 16 2019 at 04:27):

that is shadowing the real X

view this post on Zulip Mii Nguyen (Apr 16 2019 at 04:27):

Screen-Shot-2019-04-16-at-11.27.14.png

view this post on Zulip Johan Commelin (Apr 16 2019 at 04:27):

Remove those variable lines

view this post on Zulip Mii Nguyen (Apr 16 2019 at 04:28):

Screen-Shot-2019-04-16-at-11.28.22.png

always this problem

view this post on Zulip Johan Commelin (Apr 16 2019 at 04:30):

What is the reported error?

view this post on Zulip Mii Nguyen (Apr 16 2019 at 04:30):

definition 'test' is noncomputable, it depends on 'real.discrete_field' @Johan Commelin

view this post on Zulip Mario Carneiro (Apr 16 2019 at 04:31):

add noncomputable to the definition

view this post on Zulip Johan Commelin (Apr 16 2019 at 04:31):

Ok, so write noncomputable before the def

view this post on Zulip Johan Commelin (Apr 16 2019 at 04:31):

@Mii Nguyen This problem is specific to working with real polynomials. If your field of coefficients was \Q you wouldn't see the problem.


Last updated: May 12 2021 at 05:19 UTC