A multivariate polynomial is the sum of its monomials

Stream: Is there code for X?

[Yaël Dillies]

Do we have the fact that p : MvPolynomial σ R is equal to its sum of monomials p.sum (fun i ↦ monomial i)? The corresponding statement for p : R[X] is docs#Polynomial.sum_monomial_eq, but docs#MvPolynomial.sum_monomial_eq is a completely different statement...

[Yaël Dillies]

cc @Junyan Xu since this was prompted by your comment here: https://github.com/leanprover-community/mathlib4/pull/20989/files#r1927835697

[Ruben Van de Velde]

Doesn't seem like it. (Why is that using Finsupp.sum?)

[Edward van de Meent]

(because there is no Polynomial.sum, likely?)

[Yaël Dillies]

Aha! docs#MvPolynomial.as_sum and docs#MvPolynomial.support_sum_monomial_coeff it is

[Yaël Dillies]

Ruben Van de Velde said:

Why is that using Finsupp.sum?

I was following whatever Polynomial.sum_monomial_eq was doing

[Yaël Dillies]

Would be good to make names more consistent around here

[Ruben Van de Velde]

Which is also the reverse direction of docs#MvPolynomial.support_sum_monomial_coeff just above

[Ruben Van de Velde]

(We do have Polynomial.sum, but apparently not MvPolynomial.sum)

[Eric Wieser]

Finsupp.sum is the name of MvPolynomial.sum

[Eric Wieser]

I claim the inconsistency here is because we have:

structure Finsupp where ...

def AddMonoidAlgebra := Finsupp

structure Polynomial where toFinsupp : AddMonoidAlgebra

def MvPolynomial := AddMonoidAlgebra

but we ought to have

structure Finsupp where ...

structure AddMonoidAlgebra where toFinsupp : Finsupp

abbrev Polynomial := AddMonoidAlgebra

abbrev MvPolynomial := AddMonoidAlgebra

[Junyan Xu]

Yaël Dillies said:

cc Junyan Xu since this was prompted by your comment here: https://github.com/leanprover-community/mathlib4/pull/20989/files#r1927835697

Do you have to write it as a sum? Could you not use some induction principle?

[Junyan Xu]

Maybe you should show coeffsIn is the span of elements of the form m * X^k