mathlib

e49764de - feat(linear_algebra/matrix/nonsingular_inverse): decomposition of block matrices with an invertible corner (#18847)

feat(linear_algebra/matrix/nonsingular_inverse): decomposition of block matrices with an invertible corner (#18847) This result was already in a `have` statement of an existing proof; the lemma generalizes the indices slightly to not require that the overall matrix is square.