## Stream: new members

### Topic: cubic equation

#### Mii Nguyen (Apr 16 2019 at 04:12):

I try to definite a cubic equation as a polynomial function .

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 (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

#### Mii Nguyen (Apr 16 2019 at 04:26):

@Mario Carneiro I already did this in my test

#### Johan Commelin (Apr 16 2019 at 04:26):

Do you have open polynomial in your file?

#### Mario Carneiro (Apr 16 2019 at 04:26):

I mean

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


#### Mii Nguyen (Apr 16 2019 at 04:26):

yes, this is my test

#### Mario Carneiro (Apr 16 2019 at 04:27):

no variable line

#### Mario Carneiro (Apr 16 2019 at 04:27):

that is shadowing the real X

#### Mii Nguyen (Apr 16 2019 at 04:27):

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

#### Johan Commelin (Apr 16 2019 at 04:27):

Remove those variable lines

#### Mii Nguyen (Apr 16 2019 at 04:28):

always this problem

#### Johan Commelin (Apr 16 2019 at 04:30):

What is the reported error?

#### Mii Nguyen (Apr 16 2019 at 04:30):

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

#### Mario Carneiro (Apr 16 2019 at 04:31):

add noncomputable to the definition

#### Johan Commelin (Apr 16 2019 at 04:31):

Ok, so write noncomputable before the def

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