Hi all! I'm not really familiar with the linear algebra part of mathcomp-algebra, so I wonder if the following important theorems have been proven:

- the rank-nullity theorem
- the Cayley-Hamilton theorem
- the Jordan normal form theorem

Cayley-Hamilton: https://github.com/math-comp/math-comp/blob/e565f8d9bebd4fd681c34086d5448dbaebc11976/mathcomp/algebra/mxpoly.v#L457

Xuanrui Qi said:

Hi all! I'm not really familiar with the linear algebra part of mathcomp-algebra, so I wonder if the following important theorems have been proven:

- the rank-nullity theorem
- the Cayley-Hamilton theorem
- the Jordan normal form theorem

- rank-nullity theorem:
- Cayley-Hamilton theorem as @Karl Palmskog said
- Jordan normal form theorem is not there yet, but is not far from the PR math-comp/math-comp#207 which is dealing with general reduction of endomorphism to tackle specifically diagonalisation criteria and trigonalisation in $\mathbb{C}$. Note that the Smith Normal Form is available for PIDs (and euclidean domains) in CoqEAL and parts of this must be integrated in mathcomp at some point to subsume several of the above mentioned results.

Should these be listed along the odd order theorem on the mathcomp webpage https://math-comp.github.io/?

Reynald Affeldt said:

Should these be listed along the odd order theorem on the mathcomp webpage https://math-comp.github.io/?

Follow up on this question in topic https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/Documenting.20mathcomp.20theorems

Last updated: Jul 23 2024 at 21:01 UTC