---

Step * 1 of Lemma expand-det-by-row

.....subterm..... T:t
2:n
1. n : ℕ
2. i : ℕn
3. r : CRng
4. M : Matrix(n;n;r)
5. |M'| = (Σ(r) 0 ≤ i@0 < n. if isEven(i@0 + i) then M'[i@0,i] else -r M'[i@0,i] fi  * |matrix-minor(i@0;i;M')|) ∈ |r|
⊢ |M| = |M'| ∈ |r|
BY
{ Auto }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  n  :  \mBbbN{}
2.  i  :  \mBbbN{}n
3.  r  :  CRng
4.  M  :  Matrix(n;n;r)
5.  |M'|
=  (\mSigma{}(r)  0 
                \mleq{}  i@0 
                <  n
        if  isEven(i@0  +  i)  then  M'[i@0,i]  else  -r  M'[i@0,i]  fi    *  |matrix-minor(i@0;i;M')|)
\mvdash{}  |M|  =  |M'|


By

---

Latex:
Auto

---

Home Index