Commit 2023-06-02 15:44 ea247a56

View on Github →

chore: forward-port leanprover-community/mathlib#19117 (#4549)

Estimated changes

Modified Mathlib/Data/Matrix/Notation.lean

added theorem Matrix.submatrix_updateColumn_succAbove

added theorem Matrix.submatrix_updateRow_succAbove

Modified Mathlib/LinearAlgebra/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