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