Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.det_one_add_col_mul_row

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_one_add_col_mul_rowView on Github →
2022-03-17 18:31
src/linear_algebra/matrix/determinant.lean
feat(linear_algebra/matrix): The Weinstein–Aronszajn identity (#12767) …
Modified matrix.det_one_add_col_mul_rowView on Github →
2022-03-15 14:10
src/linear_algebra/matrix/determinant.lean
feat(linear_algebra/matrix/determinant): special case of the matrix determinant lemma (#12682)
Added matrix.det_one_add_col_mul_rowView on Github →