Stream: math-comp users

Topic: Mapping a polynomial to the sequence of its roots

view this post on Zulip Yves Bertot (May 19 2021 at 12:47):

I would like a function that maps any polynomial to a sequence of its roots. I guess this is possible in a rcf type. there exist the "root" predicate from poly.v, but this does not require any property from the ambient type and does not provide the result. I did some work with Bernstein coefficients on the topic in the past, but I would expect this to be subsumed by results already in math-comp.

Last updated: Jul 15 2024 at 21:02 UTC