Contribute Schur decomposition

Stream: mathlib4

[Gordon Hsu]

Hi, I am a programmer working in the semiconductor industry. My GitHub handle is kuotsanhsu. I have been learning about Lean4 in my spare time, and I am convinced that the industry can benefit from certified programming a la Adam Chlipala. Recently, I tried contributing to the HepLean project, and I formalized the Schur decomposition during the process. I would like to upstream Matrix.schur_triangulation to Mathlib. Since this is my first time contributing to Mathlib, how should I go about this? Also, is anyone working on formalizing the Jordan normal form? If not, I would like to give it a try.

[Luigi Massacci]

See here for the contribution guide, and for github access you just need to wait for an admin to click on this thread. If it doesn’t happen in a reasonable timeframe, ask on #mathlib4 > github permission

[Kim Morrison]

@Gordon Hsu, would you mind adding your github handle to your zulip profile information? It's often helpful for reviewers.

[Kim Morrison]

@Gordon Hsu, please check your (email) inbox for the invitation.

[Gordon Hsu]

Thanks, I have created PR#20730. Could someone review it?

[David Loeffler]

Also, is anyone working on formalizing the Jordan normal form? If not, I would like to give it a try.

Tagging @Alex Brodbelt who has been looking at this.

[Alex Brodbelt]

I have only formalized the 2x2 case (essentially by brute force), the general nxn case I have not touched.

[Alex Brodbelt]

I was thinking of classifying nilpotent matrices and proving some results about these, but haven't got round to this and I am not sure I will any time soon.

[Gordon Hsu]

I see, here's what I will try:

As commented by Kevin Buzzard somewhere in Zulip and the Mathlib doc, I shall start with Mathlib.LinearAlgebra.JordanChevalley and prove the case where the linear map has just one eigenvalue, i.e., the argument k to Module.End.HasGenEigenvector is Module.finrank R E for f : Module.End R E. Then, generalize to linear maps with more than one eigenvalues by way of DirectSum.Decomposition. From my experience with proving the Schur decomposition, it's easier to start with linear maps. Then, the decomposition of a matrix can be justified with Matrix.toEuclideanLin.