Commit 2024-06-03 16:18 3438911a

feat(Matrix/Determinant): add submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det (#13475) Let M be a (n+1) × n matrix whose row sums to zero. This PR proves that all the matrices obtained by deleting one row have the same determinant up to a sign (and a similar result for columns). This PR also move Mathlib/LinearAlgebra/Matrix/Determinant.lean to Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean and put the new result in a new file: Mathlib/LinearAlgebra/Matrix/Determinant/Misc.lean where various results about determinant should be added.