Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.lower_two_block_triangular_det

Modification history

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