mathlib3

996a8530 - feat(linear_algebra/matrix/nonsingular_inverse): interchange of matrix reindexing and inversion (#18812)

feat(linear_algebra/matrix/nonsingular_inverse): interchange of matrix reindexing and inversion (#18812) This follows the strategy taken in #13827, which gives us all of: * `is_unit (A.submatrix e₁ e₂) ↔ is_unit A` * `(A.submatrix e₁ e₂)⁻¹ = (A⁻¹).submatrix e₂ e₁` * `⅟(A.submatrix e₁ e₂) = (⅟A).submatrix e₂ e₁` * `invertible (A.submatrix e₁ e₂) ≃ invertible A` Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>