Redefining polynomial

Stream: mathlib4

[Yaël Dillies]

Adam Topaz said:

Yeah, I agree with that…. unless we want to redefine Polynomial;)

I am considering doing just that, actually, but I am not sure it will go in the direction you are thinking

[Johan Commelin]

What is the direction you are thinking of?

[Yaël Dillies]

Johan Commelin said:

What is the direction you are thinking of?

My current flight plan is:

1. Make docs#MonoidAlgebra irreducible. This is #25273.
2. Redefine Polynomial R := AddMonoidAlgebra R ℕ
3. Generalise as much Polynomial/MvPolynomial API to AddMonoidAlgebra, potentially removing the Polynomial/MvPolynomial special cases
4. Consider whether there is still enough duplicated Polynomial/MvPolynomial API that it is worth redefining again Polynomial R := MvPolynomial R Unit := AddMonoidAlgebra R (Unit →₀ ℕ). I expect the answer will be "no".

[Notification Bot]

A message was moved here from #mathlib4 > Notation for polynomial variables by Eric Wieser.

[Jovan Gerbscheid]

Note that the proposed fix in #mathlib4 > to_additive on AddMonoidWithOne may help to define AddMonoidAlgebra from MonoidAlgebra automatically.