polynomials

Stream: mathlib4

[Alexandre Rademaker]

For a computer scientist, not a mathematician, what material can you suggest to understand how to work with polynomials in Lean?

In particular, I am trying to formalize a problem that ask to prove that a given polynomial has not positive roots. The terms of this polynomials are taken from a sequence a1, a2,..., an, so I need to construct a polynomial using ∑ and ∏. I hope this is not too vague.

[Jireh Loreaux]

Are you simply trying to construct aₙ • xⁿ + ... + a₁ • x + a₀?

[Yury G. Kudryashov]

Do you need a single-variable polynomial or a multivariable polynomial? Do you need a polynomial as an algebraic object or as a function?

[Yury G. Kudryashov]

Can you post the mathematical statement (e.g., in LaTeX) you want to prove?