Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.det_mul_add_one_comm

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.det_mul_add_one_commView on Github →
2022-03-17 18:31
src/linear_algebra/matrix/nonsingular_inverse.lean
feat(linear_algebra/matrix): The Weinstein–Aronszajn identity (#12767) …
Added matrix.det_mul_add_one_commView on Github →