Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.det_from_blocks_zero₁₂

Modification history

2022-03-17 18:31
src/linear_algebra/matrix/determinant.lean
feat(linear_algebra/matrix): The Weinstein–Aronszajn identity (#12767) …
Added matrix.det_from_blocks_zero₁₂View on Github →