---

Step * 2 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|
6. j : ℕn
⊢ if isEven(i + j) then M[i,j] else -r M[i,j] fi  = if isEven(j + i) then M'[j,i] else -r M'[j,i] fi  ∈ |r|
BY
{ RepeatFor 2 ((EqCDA THEN 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')|)
6.  j  :  \mBbbN{}n
\mvdash{}  if  isEven(i  +  j)  then  M[i,j]  else  -r  M[i,j]  fi 
=  if  isEven(j  +  i)  then  M'[j,i]  else  -r  M'[j,i]  fi 


By

---

Latex:
RepeatFor  2  ((EqCDA  THEN  Auto))

---

Home Index