Commit 2023-04-21 14:27 e49764de
View on Github →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.