---

Step * 2 1 1 of Lemma adjugate-property

.....assertion..... 
1. r : CRng
2. n : ℕ
3. ¬(n = 0 ∈ ℤ)
⊢ ∀M:Matrix(n;n;r)
    (|M| = (Σ(r) 0 ≤ i < n. if isEven(i + 0) then M[0,i] else -r M[0,i] fi  * |matrix-minor(0;i;M)|) ∈ |r|)
BY
{ (Auto
   THEN (RWO "matrix-det-is-determinant" 0 THENA Auto)
   THEN RW (AddrC [2] (UnfoldC `determinant`)) 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN Fold `determinant` 0
   THEN Reduce 0
   THEN AutoSplit) }

1
1. r : CRng
2. n : ℕ
3. ¬n < 1
4. ¬(n = 0 ∈ ℤ)
5. M : Matrix(n;n;r)@i
⊢ (Σ(r) 0 
        ≤ i 
        < (n - 1) + 1
    if isEven(i) then M[0,i] else -r M[0,i] fi  * (determinant(n - 1;r) matrix-minor(0;i;M)))
= (Σ(r) 0 
        ≤ i 
        < n
    if isEven(i + 0) then M[0,i] else -r M[0,i] fi  * (determinant(n - 1;r) matrix-minor(0;i;M)))
∈ |r|

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (RWO  "matrix-det-is-determinant"  0  THENA  Auto)
  THEN  RW  (AddrC  [2]  (UnfoldC  `determinant`))  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  Fold  `determinant`  0
  THEN  Reduce  0
  THEN  AutoSplit)

---

Home Index