Description: The determinant function is alternating regarding rows: if a matrix has two identical rows, its determinant is 0. Corollary 4.9 in Lang p. 515. (Contributed by SO, 10-Jul-2018) (Proof shortened by AV, 23-Jul-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mdetralt.d | |
|
mdetralt.a | |
||
mdetralt.b | |
||
mdetralt.z | |
||
mdetralt.r | |
||
mdetralt.x | |
||
mdetralt.i | |
||
mdetralt.j | |
||
mdetralt.ij | |
||
mdetralt.eq | |
||
Assertion | mdetralt | |