Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-31 09:30 a99f8522

View on Github →

feat(linear_algebra/matrix/adjugate): add det_eq_sum_mul_adjugate_row (#19117) From lean-matrix-cookbook

Estimated changes

Modified src/data/matrix/notation.lean

added theorem matrix.submatrix_update_column_succ_above

added theorem matrix.submatrix_update_row_succ_above

Modified src/linear_algebra/matrix/adjugate.lean

added theorem matrix.adjugate_fin_succ_eq_det_submatrix

added theorem matrix.det_eq_sum_mul_adjugate_col

added theorem matrix.det_eq_sum_mul_adjugate_row