Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.upper_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.upper_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)
Modified matrix.upper_two_block_triangular_detView on Github →
2021-05-15 14:21
src/linear_algebra/determinant.lean
refactor(linear_algebra/matrix): split matrix.lean into multiple files (#7593) …
Modified matrix.upper_two_block_triangular_detView on Github →
2021-03-17 19:18
src/linear_algebra/determinant.lean
refactor(linear_algebra/determinant): refactor proof of upper_two_block_triangular_det (#6690) …
Modified matrix.upper_two_block_triangular_detView on Github →
2021-03-10 20:43
src/linear_algebra/determinant.lean
feat(linear_algebra/determinant): determinant of a block triangular matrix (#6050) …
Added matrix.upper_two_block_triangular_detView on Github →