# Zulip Chat Archive

## Stream: maths

### Topic: Refactoring polynomials

#### Johan Commelin (Jan 27 2020 at 12:21):

I'm starting a new thread on this topic. For reference, @Yury G. Kudryashov wrote a proposal over here: #1864

A lot of previous discussion is over here: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Algebraic.20geometry.20course/near/186673407

#### Johan Commelin (Jan 27 2020 at 12:22):

One thing that I would really like to have is given `f : polynomial R`

and `r : R`

, that `f r`

becomes `f.eval r`

. I guess that is possible with `coe_to_fun`

.

However... can we do a similar thing for mv polynomials, and maintain readability?

#### Johan Commelin (Jan 27 2020 at 12:23):

This would require some hackery, because it requires a linear ordering on `σ`

#### Johan Commelin (Jan 27 2020 at 12:24):

Suppose that `f : mv_polynomial (fin 3) R`

. Then I would love to be able to write `f [r₁, r₂, r₃]`

.

#### Johan Commelin (Jan 27 2020 at 12:24):

Is there any chance we can make that happen?

#### Johan Commelin (Jan 27 2020 at 12:29):

Should we add special support for polynomials in `n : ℕ`

variables?

#### Kevin Buzzard (Jan 27 2020 at 12:31):

I've been doing algebraic geometry and I'm just at the point where I want to talk about polynomials in n variables. I don't really know what to do. I know what theorems I want to prove but I'm still very confused about what exactly is being suggested. I would happily start refactoring `mv_polynomial`

if someone said "here's the definitions, here are ten theorems, can you prove then?" but I don't know where to start if I don't have definitions.

#### Yury G. Kudryashov (Jan 27 2020 at 20:18):

I think, a good first step would be to move `algebra`

below `polynomial`

s in the `import`

chain. This means moving `aeval`

to polynomials.

#### Yury G. Kudryashov (Jan 27 2020 at 20:20):

The next step is to define `monoid_algebra`

(e.g., as `finsupp`

or `dfinsupp`

) and prove the universal property (is it already in `finsupp`

?).

#### Yury G. Kudryashov (Jan 27 2020 at 20:24):

@Johan Commelin We have `fin.cons`

#### Yury G. Kudryashov (Jan 27 2020 at 20:25):

It has the desired type but lacks notation.

Last updated: May 12 2021 at 07:17 UTC