cubic equation

Stream: new members

[Mii Nguyen]

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.

[Mario Carneiro]

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

[Mii Nguyen]

@Mario Carneiro I already did this in my test

[Johan Commelin]

Do you have open polynomial in your file?

[Mario Carneiro]

I mean

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

[Mii Nguyen]

yes, this is my test

[Mario Carneiro]

no variable line

[Mario Carneiro]

that is shadowing the real X

[Mii Nguyen]

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

[Johan Commelin]

Remove those variable lines

[Mii Nguyen]

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

always this problem

[Johan Commelin]

What is the reported error?

[Mii Nguyen]

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

[Mario Carneiro]

add noncomputable to the definition

[Johan Commelin]

Ok, so write noncomputable before the def

[Johan Commelin]

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