Is there anything on multivariate polynomials either in the basic library or in the AFP? Or at least on bivariate polynomials?

A quick search led me to the theory Polynomial and the archive Hilbert's Nullstellensatz. Both are difficult to parse due to the lack of comments, but I assume they deal only with univariate polynomials. Am I right?

They are multivariate, see http://www.andreas-lochbihler.de/pub/haftmann14iw.pdf (or the slides) that explains the main ideas.

I found polynomials very painful to use(you need to understand the construction, otherwise sledgegammer does not work) when I needed them, but it works.

Some less negative comment: I used polynomials and needed very practical theorems (is x in the variables of the polynom 1? -- no this is not automatic). I did not need any analysis. The library was developed for the latter, not for my use case.

@Mathias Fleury: Anthony was linking to the `Polynomial`

theory from `HOL-Computational_Algebra`

, which is univariate. What you're thinking of is the `Polynomials`

entry in the AFP.

I use the latter in my entries on symmetric polynomials and power sum polynomials, and I heavily use the first of those in my proof of the transcendence of $\pi$. But yes, they are very painful to use and there's a lot of stuff missing.

There might be a lot of material in my entries that should be moved to the `Polynomials`

entry as well.

ah yeah, true, sorry for the confusion.

I forgot that we have at least 2 different libraries of polynomials...

That's a very optimistic estimate. :P

There's at least 3 more in HOL-Algebra.

The univariate ones from `HOL-Computational_Algebra`

are by far the most pleasant ones to use, but, well, they are univariate. And they are bound to the type classes, like everything in `HOL-Computational_Algebra`

.

Mathias Fleury said:

They are multivariate, see http://www.andreas-lochbihler.de/pub/haftmann14iw.pdf (or the slides) that explains the main ideas.

Thanks for the reference.

When using univariate polynomials, should one see them as particular cases of multivariate polynomials or is there one of the many formalizations of univariate polynomials which is compatible with multivariate polynomials as formalized in `Polynomials`

?

I don't think there is one that is compatible to that. But I would say if you can use the ones from `HOL-Computational_Algebra`

, you should use those.

There's also some work on bivariate polynomials that sees them as `'a poly poly`

.

(where `poly`

is the type from `HOL-Computational_Algebra`

)

(deleted)

(deleted)

Last updated: Aug 13 2022 at 05:18 UTC