Polynomial from coefficients

Stream: Is there code for X?

[Eric Wieser]

#9011 adds

/-- The associated polynomial `(v 0) + (v 1) * X + ... + (v (n-1)) * X ^ (n-1)` to `matrix.circulant v`.-/
noncomputable
def matrix.circulant.poly [semiring α] (v : fin n → α) : polynomial α :=
∑ i : fin n, polynomial.monomial i (v i)

Obviously it doesn't belong in the matrix namespace as #9011 has it, but do we have this "make a polynomial from its coefficients" function somewhere already?

[Eric Wieser]

cc @Alex Zhang

[Johan Commelin]

Oops, I missed this.

[Johan Commelin]

Anyway, I think that this sum is the best we've got, when it comes to constructing a polynomial from its coefficients

[Eric Wieser]

Presumably there's a docs#finsupp_of_finite somewhere, which can be composed with docs#finsupp.map_domain

[Eric Wieser]

Which would make the coefficients defeq

[Eric Wieser]

Ah, it's docs#finsupp.equiv_fun_on_fintype

[Johan Commelin]

Aah, I agree that this is a better idea.

[Johan Commelin]

Presumably we should have polynomial.mk_of_fin or something like that?

[Eric Wieser]

Yeah, or mk_of_fin_coeffs