polynomials from coefficient

Stream: maths

[Johan Commelin]

Suppose I have a bunch of coefficients a 0, a 1, a 2, ..., a n, probably implemented as a : nat -> R for some ring R. What is the best way to turn this into the polynomial $\sum_{i < n} a_i X^i$?
One can simply write

(finset.range n).sum (λ i, (a i : R[X]) * X ^ i)

But this has the disadvantage that is ins't very structured. For example, showing that the i-th coefficient is a i is not a 1-lemma application. Should we have a dedicated constructor for this? Or does something already exist?

[Yakov Pechersky]

You turn "a" into a finsupp, and use polynomial.of_finsupp

[Yakov Pechersky]

Unfortunately I'm wrong and we don't have that constructor. Can you make an add_monoid_algebra from your "a"?

[Johan Commelin]

Afaik, we really don't have a good constructor + API for this type of examples.

[Riccardo Brasca]

If P : ℕ →₀ R then polynomial.of_finsupp P should give the polynomial, doesn't it?

[Riccardo Brasca]

I just realized that your question is probably related to #12447 :face_palm:

[Junyan Xu]

There is no polynomial.of_finsupp P because what you want is simply ⟨P⟩.

structure polynomial (R : Type u_1) [semiring R] : Type u_1
    (to_finsupp : add_monoid_algebra R ℕ)
add_monoid_algebra k G = (G →₀ k)

[Kevin Buzzard]

One should rename the constructor of_finsupp using the :: syntax

[Eric Wieser]

src#polynomial

[Eric Wieser]

Sebastien Gouezel went back in time and renamed it for you

[Kevin Buzzard]

Nice! I didn't know he could do that.

[Eric Wieser]

So more accurate would be "the docs do not list a polynomial.of_finsupp because it is a structure constructor like sigma.mk"

[Yakov Pechersky]

So I wasn't insane thinking we had one in the first place...

[Kevin Buzzard]

It depends if you thought it before Sebastien went back in time.