!4#4106 port RingTheory.PolynomialAlgebra

Stream: PR reviews

[Damiano Testa]

I opened the PR !4#4106, but I do not see it in the list of open mathlibport PRs. Since this is my first mathlib port file, I just wanted to make sure that I am not doing anything wrong! Thanks!

[Yaël Dillies]

Have you waited 30min?

[Damiano Testa]

Ah, not yet I guess! :upside_down:

[Damiano Testa]

With the help of @Chris Hughes this PR is ready!

As it is my first port from scratch, I would welcome any comments about style and guidelines! Thanks!