Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.from_blocks_eq_of_invertible₂₂

Modification history

2023-04-24 09:08
src/linear_algebra/matrix/nonsingular_inverse.lean
refactor(linear_algebra/matrix/nonsingular_inverse): move results about block matrices to `schur_complement` (#18850) …
Modified matrix.from_blocks_eq_of_invertible₂₂View on Github →
2023-04-21 14:27
src/linear_algebra/matrix/nonsingular_inverse.lean
feat(linear_algebra/matrix/nonsingular_inverse): decomposition of block matrices with an invertible corner (#18847) …
Added matrix.from_blocks_eq_of_invertible₂₂View on Github →