Polynomial vs MvPolynomial

Stream: Is there code for X?

[Antoine Chambert-Loir]

Is there somewhere in Mathlib the algebraic equivalence of Polynomial R with MvPolynomial Unit R — the unique e : AlgEquiv (Polynomial R) (MvPolynomial Unit R) that sends Polynomial.X to MvPolynomial.X default — as well as the comparison between this isomorphism and evaluations?

[Yaël Dillies]

docs#MvPolynomial.pUnitAlgEquiv

[Yaël Dillies]

I do not know about the evaluation part

[Antoine Chambert-Loir]

At this point, it's not hard

[Jireh Loreaux]

Why is that stated with pUnit instead of an arbitrary type with a Unique instance?

[Jz Pan]

Yaël Dillies said:

I do not know about the evaluation part

That should be provable just by simp since MvPolynomial.pUnitAlgEquiv has @[simps] lemma

[Yaël Dillies]

Not sure what you mean. eval is not a projection of polynomials (nor of mv polynomials). simps only generates lemmas for projections (although it would be cool if that could be extended)

[Antoine Chambert-Loir]

Anyway, the lemma is in the PR for evaluation of power series. #15019, I believe.