Computable MvPolynomial discussion

Stream: mathlib4

[Julian Sutherland]

We still have to implement degree and eval, but this should be done soon! :slight_smile:

[tsuki（Hao Shen)]

Great to see your work! Could you please provide some computable examples?

[Wrenna Robson]

František Silváši 🦉 said:

Hey, we've finished a formalisation of computable polynomials, pending some cleanups.

We have an Equiv between MvPolynomial and a quotient of ExtTreeMap that never maps to zero. In other words, this interprets finitely supported functions computationally as finite maps.

Importantly, we also have the full RingEquiv against mathlib's MvPolynomial.

Of course, feedback more than welcome, although please note that this was just recently finished and needs a cleanup pass, which I hope to get around to during the weekend or this coming Monday :).

This looks cool. Can I ask, it looks like you are able to have monomials with the same power repeated more than once, which I would have thought might give you problems. Is this the case?

[Notification Bot]

3 messages were moved here from #announce > Computable MvPolynomial + RingEquiv with MvPolynomial by Riccardo Brasca.

[Riccardo Brasca]

Feel free to continue the discussion here!