Yves Bertot (May 19 2021 at 12:47): 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: Feb 08 2023 at 08:02 UTC