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