---

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

.....subterm..... T:t
3: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
⊢ |matrix-minor(i;j;M)| = |matrix-minor(j;i;M')| ∈ |r|
BY
{ (RWO "transpose-matrix-minor<" 0 THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
3: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{}  |matrix-minor(i;j;M)|  =  |matrix-minor(j;i;M')|


By

---

Latex:
(RWO  "transpose-matrix-minor<"  0  THEN  Auto)

---

Home Index