Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-15 14:10 7582e149

View on Github →

feat(linear_algebra/matrix/determinant): special case of the matrix determinant lemma (#12682)

Estimated changes

Modified src/linear_algebra/matrix/determinant.lean

added theorem matrix.det_one_add_col_mul_row

added theorem matrix.lower_two_block_triangular_det

modified theorem matrix.upper_two_block_triangular_det