Yves Bertot (Jul 13 2021 at 07:27): Yves Bertot (Jul 13 2021 at 07:27):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?
Cyril Cohen (Jul 13 2021 at 09:14):Yes, see what I did in the spectral PR
Cyril Cohen (Jul 13 2021 at 09:14): Cyril Cohen (Jul 13 2021 at 09:21):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?
Pierre-Yves Strub (Jul 13 2021 at 09:21):Hmmm. I think we defined this in our library about elliptic curves
Pierre-Yves Strub (Jul 13 2021 at 09:22):I'll check
Cyril Cohen (Jul 13 2021 at 09:22):But somehow, in the PR math-comp/math-comp#207 the functions spectral_diag does it :laughter_tears:
Cyril Cohen (Jul 13 2021 at 09:23):It gives the row vector of eigenvalues of a diagonalizable matrix.
Yves Bertot (Jul 13 2021 at 09:45):@Mohit Tekriwal , this may be useful for you!
Mohit Tekriwal (Jul 13 2021 at 10:13):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: Apr 20 2024 at 05:01 UTC