Functoriality of MvPolynomial

Stream: Is there code for X?

[Nailin Guan]

I found we only have MvPolynomial.map for functoriality on the ring, what about the index set? Since I am trying to push the result "Power series over regular local ring is regular" to MvPolynomial, I am missing the stable under isomorphic change of index and induction step.

[Floris van Doorn]

Hmm... It's surprising to me, but that seems to be missing.

[Floris van Doorn]

@loogle |- MvPolynomial _ _ →+* MvPolynomial _ _

[loogle]

:search: MvPolynomial.map, MvPolynomial.iterToSum, and 3 more

[Riccardo Brasca]

It's MvPolynomial.rename.

[Riccardo Brasca]

For power series on the other hand the API is much smaller. There is #33188 by @Bingyu Xia that is on my review list (sorry for being very slow).

[Nailin Guan]

Sorry, I need power series in the first place, but you solved it also. Thanks

[Nailin Guan]

Sorry, maybe not a very appropriate place, but what is happening here?
图片.png

[Yiming Fu]

Nailin Guan said:

Sorry, maybe not a very appropriate place, but what is happening here?
图片.png

I think Lean tried but failed to compile this instance because MvPolynomial is noncomputable, so the instance needs to be marked as noncomputable.

[Riccardo Brasca]

Yes, most likely due to some noncomputable thing.