# Zulip Chat Archive

## Stream: new members

### Topic: Examples of mv_polynomials

#### YurySerdyuk (Jun 21 2023 at 13:34):

Hi, I am a complete newbie with Lean, but I would like to prove some properties of simple programs dealing with the multivariate polynomials.

At first, I would like to create the examples of polynomials and to do some operations on them.

My first attempt was :

import data.mv_polynomial.comm_ring

variables x y : ℕ

def p1 : mv_polynomial (fin 2) ℚ := x^3 * y + 1

def p2 : mv_polynomial (fin 2) ℚ := x * y + x + y + 1

#eval p1 + p2

What is wrong with my code ? The answer of Lean was

missing 'noncomputable' modifier, definition 'p1' depends on 'mv_polynomial.comm_ring'

#### Eric Wieser (Jun 21 2023 at 13:36):

Lean is telling you to write `noncomputable`

before the word `def`

; but you can also just write `noncomputable theory`

near the top of the file

#### Eric Wieser (Jun 21 2023 at 13:36):

But those aren't the polynomials you think they are; those are families of *constant* polynomials parametrized by `x, y`

#### Eric Wieser (Jun 21 2023 at 13:37):

The two generators of your polynomial are actually `mv_polynomial.X 0`

and `mv_polynomial.X 1`

#### YurySerdyuk (Jun 21 2023 at 13:51):

def p1 : mv_polynomial (fin 2) ℚ := mv_polynomial.X 3

def p2 : mv_polynomial (fin 2) ℚ := mv_polynomial.X 2

#eval p1 + p2

code generation failed, VM does not have code for 'classical.choice'

#### Matthew Ballard (Jun 21 2023 at 13:53):

`mv_polynomial`

does not currently generate any executable computer code

#### Eric Rodriguez (Jun 21 2023 at 13:54):

The way polynomials are implemented doesn't let you use #eval to see them, but you can definitely prove whatever you want about p1 and p2

#### Matthew Ballard (Jun 21 2023 at 13:54):

When you call `#eval`

you ask your computer to do a computation which is not possible with the design

#### Eric Rodriguez (Jun 21 2023 at 13:55):

Also note that the number is not a power, it's the index: we tend to use X and Y in pen and paper for 2 degrees but because computers, we have to write X_0, X_1

Last updated: Dec 20 2023 at 11:08 UTC