Stream: math-comp users

Topic: Important theorems about linear algebra?

Xuanrui Qi (Jan 26 2021 at 20:48):

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

Karl Palmskog (Jan 26 2021 at 22:26):

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

Cyril Cohen (Jan 27 2021 at 01:30):

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:
  • matrix version
  • vector space version
• 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.

Reynald Affeldt (Jan 27 2021 at 02:17):

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

Cyril Cohen (Jan 27 2021 at 14:23):

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: Jan 29 2023 at 19:02 UTC