In an algebraically closed field, there should be a function mapping any polynomial to a sequence of its roots (counted with multiplicity). Where do I find such a function in math-comp?
I ask the question because the ultimate goal is to talk about the eigenvalues of a matrix with complex coefficients. Any ideas?
Yes, see what I did in the spectral PR
sorry the function you want is not there actually... @Pierre-Yves Strub has a version of it for decidable fields I think. Maybe he can point it out?
Hmmm. I think we defined this in our library about elliptic curves
But somehow, in the PR math-comp/math-comp#207 the functions
spectral_diag does it :laughter_tears:
It gives the row vector of eigenvalues of a diagonalizable matrix.
@Mohit Tekriwal , this may be useful for you!
Thanks @Yves Bertot ! I will look into it. Is
spectral.v the file I should be looking into ? It contains the definition
spectral_diag that @Cyril Cohen is pointing to, I guess
Last updated: Aug 19 2022 at 20:03 UTC