Polynomial.Basic - instance semiring

Stream: new members

[Xavier Généreux]

Hello everyone!

I am trying to understand why the semiring instance in the Polynomial.Basic file doesn't use the fact that it is a semiring from MonoidAlgebra.Basic. In my understanding, Polynomial is just a special case, so why is it using this proof? Is it only because of speed issues as mentioned in #7432?

[Ruben Van de Velde]

This seems to have been changed in https://github.com/leanprover-community/mathlib/commit/3a5c8711beeadc4ec0bb90838c7854c68b2accc1#diff-4ad03e2885a87324092e94b0e0ef5c02ae35ea4dc3a9adf02d57031b8577bcba

[Yaël Dillies]

There's something mathematically wrong here. Namely, Polynomial should be an abbrev for AddMonoidAlgebra, and AddMonoidAlgebra a one-field structure wrapper around Finsupp

[María Inés de Frutos Fernández]

@Sébastien Gouëzel

[Damiano Testa]

After this being brought up so many times, I will try to actually start on the change. It might take a few iterations.

[Damiano Testa]

The plan is to place the structure divide when defining AddMonoidAlgebra, right? I remember that @Eric Wieser had suggested even trying to unify AddMonoidAlgebra and MonoidAlgebra: these two refactors should not happen at the same time!

[Damiano Testa]

I cannot move across streams, so this is where the conversation is now.