Description: The determinant of a submatrix of a square matrix obtained by removing a row and a column at the same index equals the determinant of the original matrix with the row replaced with 0's and a 1 at the diagonal position. (Contributed by AV, 31-Jan-2019) (Proof shortened by AV, 24-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | smadiadet.a | |
|
smadiadet.b | |
||
smadiadet.r | |
||
smadiadet.d | |
||
smadiadet.h | |
||
Assertion | smadiadet | |