mathlib3

a07a7ae9 - refactor(linear_algebra/matrix/nonsingular_inverse): move results about block matrices to `schur_complement` (#18850)

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.