Stream: math-comp analysis

Topic: roots of polynomial in algebraically closed field


view this post on Zulip 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?

view this post on Zulip Cyril Cohen (Jul 13 2021 at 09:14):

Yes, see what I did in the spectral PR

view this post on Zulip Cyril Cohen (Jul 13 2021 at 09:14):

math-comp/math-comp#207

view this post on Zulip 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?

view this post on Zulip Pierre-Yves Strub (Jul 13 2021 at 09:21):

Hmmm. I think we defined this in our library about elliptic curves

view this post on Zulip Pierre-Yves Strub (Jul 13 2021 at 09:22):

I'll check

view this post on Zulip 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:

view this post on Zulip Cyril Cohen (Jul 13 2021 at 09:23):

It gives the row vector of eigenvalues of a diagonalizable matrix.

view this post on Zulip Yves Bertot (Jul 13 2021 at 09:45):

@Mohit Tekriwal , this may be useful for you!

view this post on Zulip 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: Aug 19 2022 at 20:03 UTC