---

Step * of Lemma expand-det-by-row

∀[n:ℕ]. ∀[i:ℕn]. ∀[r:CRng]. ∀[M:Matrix(n;n;r)].
  (|M| = (Σ(r) 0 ≤ j < n. if isEven(i + j) then M[i,j] else -r M[i,j] fi  * |matrix-minor(i;j;M)|) ∈ |r|)
BY
{ (InstLemma `expand-det-by-column` []
   THEN RepeatFor 3 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN (D -2 With ⌜M'⌝  THENA Auto)
   THEN NthHypEq (-1)
   THEN EqCDA) }

1
.....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|

2
.....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|
⊢ (Σ(r) 0 
        ≤ j 
        < n
    if isEven(i + j) then M[i,j] else -r M[i,j] fi  * |matrix-minor(i;j;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|

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[i:\mBbbN{}n].  \mforall{}[r:CRng].  \mforall{}[M:Matrix(n;n;r)].
    (|M|  =  (\mSigma{}(r)  0  \mleq{}  j  <  n.  if  isEven(i  +  j)  then  M[i,j]  else  -r  M[i,j]  fi    *  |matrix-minor(i;j;M)|))


By

---

Latex:
(InstLemma  `expand-det-by-column`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  (D  -2  With  \mkleeneopen{}M'\mkleeneclose{}    THENA  Auto)
  THEN  NthHypEq  (-1)
  THEN  EqCDA)

---

Home Index