matrix det

Stream: Is there code for X?

[Alex Zhang]

Is there any code for " the det of a square matrix is the product of its eigenvalues"?

[Kevin Buzzard]

You have to be careful what you mean by eigenvalues here, for example there are issues with multiplicities and with eigenvalues not being defined over the base field. What I'm saying is that you are asking for a proof but it might even be nontrivial to write down the statement. Why not try it?

[Alex Zhang]

Yeah, it is not trivial to formalise the statement. I was just being lazy here to ask for any existing code.
I will try to write it down myself.

[Anne Baanen]

We have docs#det_eq_sign_char_poly_coeff, but nothing connecting the characteristic polynomial and eigenvalues as far as I know.

[Kevin Buzzard]

What we would need here is a theory of algebraic (and geometric?) multiplicities of eigenvalues. The geometric multiplicity is the dimension of the eigenspace. The algebraic multiplicity is the dimension of the generalised eigenspace. Do we have either of these?

[Adam Topaz]

We have both docs#module.End.eigenspace and docs#module.End.generalized_eigenspace

[Kevin Buzzard]

That's not the generalised eigenspace because it takes an extra parameter

[Adam Topaz]

You're right, of course, and we also have this (with a strange name) docs#module.End.maximal_generalized_eigenspace

[David Wärn]

Probably what you need is that multiplicity of a root in the characteristic polynomial equals dimension of generalised eigenspace

[Kevin Buzzard]

A natural proof of this would go via structure theorem of f.g. modules over a PID.

[Kevin Buzzard]

and also the theory of internal direct sums, which I will get around to at some point

[David Wärn]

It's natural but maybe a sledgehammer?

[David Wärn]

If you have a subspace $U \subseteq V$ and an endomorphism $T : V \to V$ which restricts to $T' : U \to U$, then there's is also an endomorphism $\bar T : V/U \to V/U$, and $det(T) = det(T') det(\bar T)$. The generalised eigenspace in an example of such a $U$, so this expresses the char poly as a product

[David Wärn]

The eigenvalue is not a root of the second poly (since the corresponding matrix is invertible). But you need to prove that the char poly of a nilpotent matrix is $t^{dim(V)}$

[David Wärn]

Although for the original question you can just define the multisets of eigenvalues as the roots of the characteristic polynomial. Then you should be able to prove in mathlib that the product is the determinant?