Integral polynomials

Stream: new members

[Maxime Darrin]

Hi,
How can I define a polynomial with integral coefficients and consider its associated function and roots over the reals ?
I'm trying to use P : polynomial ℤ to define a polynomial with integral coefficients, I thought of using polynomial.to_continuous_map_on P (⊤ : set ℝ) ℝ to get its associate functions over the reals but does not seems to work
How should I do that ?

[Hanting Zhang]

docs#polynomial.aeval should work (this might not be the idiomatic way though)

[Hanting Zhang]

For roots there's docs#polynomial.roots or docs#polynomial.root_set

[Heather Macbeth]

You can use docs#polynomial.map with docs#int.cast_ring_hom to convert your int-polynomial to a real-polynomial, at which point @Hanting Zhang's suggestions for the roots will work.