Polynomials in Model Theory

Stream: mathlib4

[Aaron Anderson]

I'm looking at @Chris Hughes 's new PRs, #16503 and #16504, which prove the definability of zero loci by building terms in the language of rings to represent polynomials.

[Aaron Anderson]

While the approach definitely works, I feel like a better API is needed. Specifically, I want (and would be happy to work on constructing) one or both of the following two functions:

[Aaron Anderson]

A map from MvPolynomial κ R to Language.ring.Term (α ⊕ κ), where α is an appropriate type of coefficients. (I feel like this is implicit in #16504, but should probably be defined explicitly)

[Aaron Anderson]

A map from MvPolynomial κ R to Language.ring[[R]].Term κ, or perhaps Language.ring[[S]].Term κ for any set S containing the coefficients. In my head, this goes with an extension of parts of the ring API (for instance, the ability to add and multiply terms) to extensions of Language.ring, such as Language.ring[[R]]. I've done this with the Language.order API, where most things are just about some language L with an instance of L.IsOrdered that makes it canonically an extension of Language.order, but I don't claim that I've done that API correctly.