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

I'll check

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: Feb 05 2023 at 07:03 UTC