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: Mar 02 2024 at 17:02 UTC