Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-04-24 09:08 a07a7ae9

View on Github →

refactor(linear_algebra/matrix/nonsingular_inverse): move results about block matrices to schur_complement (#18850) This gets these out of the critical path for porting, and also balances the size of these files a little better. I've added myself second rather than last on the author list since the bulk of these moved lemmas are mine, and they are about equal in number of lines to the existing lemmas. The lemmas have been moved without modification, though the module docstring for schur_complement has been adapted accordingly.

Estimated changes