# Zulip Chat Archive

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

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 `X`

available 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):

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

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