# Zulip Chat Archive

## Stream: maths

### Topic: constructive polynomials

#### Reid Barton (Oct 12 2019 at 17:59):

I know polynomials were changed to use classical logic, and that's fine, but it occurred to me that there is a constructively correct notion of $R[X]$, and it isn't the one we were using (unless $R$ has decidable equality).

#### Johan Commelin (Oct 12 2019 at 18:06):

Which is...

#### Reid Barton (Oct 12 2019 at 18:07):

Namely, you can either take some free construction, or you can work with `list R`

modulo the relation of adding 0s to the end of the list, and I think these are constructively equivalent. Moreover, all the polynomial operations can be implemented without using equality on `R`

aside from decidable equality of polynomials (obviously) and degree (slightly less obviously, but also clearly correctly, since `deg (1 + (a - b) * X)`

is 0 iff `a = b`

).

#### Reid Barton (Oct 12 2019 at 18:09):

The second one is also a lot more reasonable for computation than the current representation, since addition is linear and not quadratic for example

#### Reid Barton (Oct 12 2019 at 18:09):

I'm not sure whether there is a compelling reason to switch at this point though

#### Johan Commelin (Oct 12 2019 at 18:12):

This doesn't easily generalize to `mv_poly`

right?

#### Johan Commelin (Oct 12 2019 at 18:13):

If anything, I would like to redefine `polynomial R`

as `mv_polynomial unit R`

, and make the two API play more in sync. There is lots of stuff that has to be done twice, and isn't done in exactly the same way, etc...

#### Reid Barton (Oct 12 2019 at 18:14):

The big free construction still works for `mv_polynomial`

, and I think you can also do something more similar to the current implementation but constructively correct, but it won't be as nice as lists

#### Reid Barton (Oct 12 2019 at 18:19):

`free_comm_ring`

is almost the "big free construction", except it needs to be `free_algebra`

, and also use `free_comm_monoid`

in place of `multiset`

#### Reid Barton (Oct 12 2019 at 18:19):

Or you can build it directly from the syntax of algebras

#### Patrick Massot (Oct 12 2019 at 18:24):

Reid, are you still checking your topology PR? It doesn't sound like it...

#### Reid Barton (Oct 12 2019 at 18:29):

I discovered that there were a sizable number of irrelevant universe parameter order changes, so I "fixed" them and rebuilt

#### Reid Barton (Oct 12 2019 at 18:32):

Oh sorry, I misremembered how `multiset`

is implemented. It is actually the correct thing already.

#### Patrick Massot (Oct 12 2019 at 18:32):

So, do you think we can merge?

#### Kenny Lau (Oct 13 2019 at 00:44):

@Reid Barton the constructive polynomials on R is R (x)_Z Z[x]

#### Yury G. Kudryashov (Oct 18 2019 at 01:22):

@Johan Commelin One-variable polynomials can be evaluated on non-commutative rings (e.g., matrices or bounded linear operators; not sure if this is implemented in mathlib), and it can't work with `mv_polynomial`

.

#### Johan Commelin (Oct 18 2019 at 05:10):

Hmm, fair enough

#### Johan Commelin (Oct 18 2019 at 05:11):

So you are saying that `polynomial`

should be defined as `mv_noncomm_polynomial unit`

?

#### Yury G. Kudryashov (Oct 19 2019 at 14:24):

AFAIK, we don't have `mv_noncomm_polynomial`

(yet).

#### Yury G. Kudryashov (Oct 19 2019 at 14:28):

Probably I'd prefer to have a few monoids of monomials, and let `*_polynomial`

be `monoid_algebra monomials_type`

.

#### Yury G. Kudryashov (Oct 19 2019 at 14:28):

Where `monoid_algebra`

is https://en.wikipedia.org/wiki/Group_ring for monoids instead of groups (I'm not sure what is the right word for this).

#### Kevin Buzzard (Oct 19 2019 at 15:41):

I've heard it being called "monoid ring" before

#### Mario Carneiro (Oct 19 2019 at 16:22):

I recall Kenny having a formalization of polynomials using quotients of ring expressions that is pretty constructive

#### Johan Commelin (Oct 19 2019 at 16:39):

@Yury G. Kudryashov I think `finsupp`

already allows you to do monoid rings

#### Johan Commelin (Oct 19 2019 at 16:40):

It's been a while that I read that part of the source though

Last updated: May 18 2021 at 06:15 UTC