---

Step * of Lemma equal-rows-det

∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)].
  |M| = 0 ∈ |r| supposing ∃i,j:ℕn. ((¬(i = j ∈ ℤ)) ∧ (matrix-swap-rows(M;i;j) = M ∈ Matrix(n;n;r)))
BY
{ ((InstLemma `det-equal-rows` [] THEN RepeatFor 3 (ParallelLast')) THEN Auto THEN ExRepD) }

1
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. ∀[i,j:ℕn].  |M| = 0 ∈ |r| supposing (¬(i = j ∈ ℤ)) ∧ (matrix-swap-rows(M;i;j) = M ∈ Matrix(n;n;r))
5. i : ℕn
6. j : ℕn
7. ¬(i = j ∈ ℤ)
8. matrix-swap-rows(M;i;j) = M ∈ Matrix(n;n;r)
⊢ |M| = 0 ∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].  \mforall{}[M:Matrix(n;n;r)].
    |M|  =  0  supposing  \mexists{}i,j:\mBbbN{}n.  ((\mneg{}(i  =  j))  \mwedge{}  (matrix-swap-rows(M;i;j)  =  M))


By

---

Latex:
((InstLemma  `det-equal-rows`  []  THEN  RepeatFor  3  (ParallelLast'))  THEN  Auto  THEN  ExRepD)

---

Home Index