MVPolynomial requires CommSemiring

Stream: mathlib4

[William Coram]

MvPolynomials are defined by the following

def MvPolynomial (σ : Type*) (R : Type*) [CommSemiring R] :=
  AddMonoidAlgebra R (σ →₀ ℕ)

On the other hand MvPowerseries does not require that R is commutative (or even a Semiring for that matter). This means we can only use truncation when we specialize R to a CommSemiring. I see no reason why this is the case?

[Yaël Dillies]

I see no reason either. Feel free to change

[Yaël Dillies]

Note that my plan in the not-so-far future is to turn docs#MvPolynomial into an abbrev and remove most of its API (in favour of the more general docs#AddMonoidAlgebra one)

[William Coram]

Sounds good. I'll try and make a PR this weekend addressing this.

[Kevin Buzzard]

docs#AddMonoidAlgebra -- indeed, only uses Semiring so refactoring the def should be easy

[William Coram]

Sounds good. I'll try and make a PR this weekend addressing this.

So this turns out to be a lot more work than expected. I may get around to this, or leave it to Yaël when they do their refactor.

[Eric Wieser]

I think we tried this many years ago

[Yury G. Kudryashov]

@Yaël Dillies Why do you think having it as an abbrev is better?

[Yaël Dillies]

My reasoning is that there are no semantic difference between MvPolynomial and AddMonoidAlgebra. A multivariate polynomial is an element of some add monoid algebra, while eg an element of an add monoid algebra can be represented as a finitely supported function.

[Yaël Dillies]

Now that Lean is becoming stricter about type synonyms, the halfway situation MvPoynomial finds itself in has become unsustainable and we need to either make it a one-field structure or an abbrev. I claim the former would bring unnecessary code duplication, while the latter is perfectly motivated by the mathematics.