Zulip Chat Archive

Stream: new members

Topic: Integral polynomials

Maxime Darrin (Jul 04 2021 at 19:21):

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 (Jul 04 2021 at 19:33):

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

Hanting Zhang (Jul 04 2021 at 19:36):

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

Heather Macbeth (Jul 05 2021 at 04:39):

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.

Last updated: Dec 20 2023 at 11:08 UTC