LinearAlgebra.GaussianElimination

Stream: mathlib4

[George Granberry]

Hej! I'm currently taking a Lean course with @Mario Carneiro and we thought a neat project for me to work on would be to formalize Gaussian Elimination. But Mario mentioned there might be some specific formats that maintainers would like to see the formalization in before I get started on it myself. Is this the correct place to post in order to get some guidance on how to structure the formalization before I get started on it myself?

[Eric Wieser]

This is definitely a sensible place to post!

[Eric Wieser]

It's possible there is some overlap here with #21018

[George Granberry]

@Mark Santa Clara Munro , it looks like you've already done a lot of work on this. Did you want a hand on it? I can't really tell from the PR how much work is roughly left.

Also @Eric Wieser if you have anything else Linear Algebra related that you'd like to see formalized I'm always open to project ideas.

[Jireh Loreaux]

I'd like to see some things related to the numerical range of a continuous linear map formalized. Of course, the Toeplitz-Hausdorff theorem, but there's other stuff that could be done. There are plenty of generalizations one could consider as well. The most general version with nice properties replaces a single vector with a selfadjoint operator, but to prove anything nice about it we would have to develop theory about majorization.

[Mark Santa Clara Munro]

Hi, I apologize for the late response @George Granberry! I talked to my research advisor, @Christopher Lynch, and although in regular situations we would love to combine efforts, but this might be something where we are too far into it. I'm not sure how much work is roughly left, but I'd like to think we're not too far off so I am not sure if it would be worth it.

[George Granberry]

@Jireh Loreaux I'd be happy to work on the Toeplitz-Hausdorff theorem if you think it is doable by someone somewhat new to Lean. If I come up with the general structure for the proof do you mind giving me some feedback to make sure I'm going in the right direction.

@Mark Santa Clara Munro No problem at all! I looked over the code and thought the same thing.