---

Step * 2 1 1 of Lemma det-fun-is-determinant


1. r : CRng
2. n : ℤ
3. 0 < n
4. d : det-fun(r;n)
5. ∀i:ℕn. ∀M:Matrix(n;n;r).
     ((d matrix+(r;i;matrix-minor(0;i;M)))
     = (if isEven(i) then d I else -r (d I) fi  * (determinant(n - 1;r) matrix-minor(0;i;M)))
     ∈ |r|)
⊢ d = (λM.((d I) * (determinant(n;r) M))) ∈ (Matrix(n;n;r) ⟶ |r|)
BY
{ ((FunExt THENA Auto)
   THEN Unfold `determinant` 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN Fold `determinant` 0
   THEN Reduce 0
   THEN AutoSplit
   THEN RenameVar `M' (-1)
   THEN (Assert ⌜(d M)
                 = (Σ(r) 0 
                         ≤ i 
                         < (n - 1) + 1
                     M[0,i] * (if isEven(i) then d I else -r (d I) fi  * (determinant(n - 1;r) matrix-minor(0;i;M))))
                 ∈ |r|⌝⋅
         THENA ((RWO "-2<" 0 THENA Auto) THEN Thin (-2) THEN (Subst' (n - 1) + 1 ~ n 0 THENA Auto))
         )) }

1
1. r : CRng
2. n : ℤ
3. ¬n < 1
4. 0 < n
5. d : det-fun(r;n)
6. M : Matrix(n;n;r)
⊢ (d M) = (Σ(r) 0 ≤ i < n. M[0,i] * (d matrix+(r;i;matrix-minor(0;i;M)))) ∈ |r|

2
1. r : CRng
2. n : ℤ
3. ¬n < 1
4. 0 < n
5. d : det-fun(r;n)
6. ∀i:ℕn. ∀M:Matrix(n;n;r).
     ((d matrix+(r;i;matrix-minor(0;i;M)))
     = (if isEven(i) then d I else -r (d I) fi  * (determinant(n - 1;r) matrix-minor(0;i;M)))
     ∈ |r|)
7. M : Matrix(n;n;r)
8. (d M)
= (Σ(r) 0 
        ≤ i 
        < (n - 1) + 1
    M[0,i] * (if isEven(i) then d I else -r (d I) fi  * (determinant(n - 1;r) matrix-minor(0;i;M))))
∈ |r|
⊢ (d M)
= ((d 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|

---

Latex:

---

Latex:

1.  r  :  CRng
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  d  :  det-fun(r;n)
5.  \mforall{}i:\mBbbN{}n.  \mforall{}M:Matrix(n;n;r).
          ((d  matrix+(r;i;matrix-minor(0;i;M)))
          =  (if  isEven(i)  then  d  I  else  -r  (d  I)  fi    *  (determinant(n  -  1;r)  matrix-minor(0;i;M))))
\mvdash{}  d  =  (\mlambda{}M.((d  I)  *  (determinant(n;r)  M)))


By

---

Latex:
((FunExt  THENA  Auto)
  THEN  Unfold  `determinant`  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  Fold  `determinant`  0
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  RenameVar  `M'  (-1)
  THEN  (Assert  \mkleeneopen{}(d  M)
                              =  (\mSigma{}(r)  0 
                                              \mleq{}  i 
                                              <  (n  -  1)  +  1
                                      M[0,i] 
                                      * 
                                      (if  isEven(i)  then  d  I  else  -r  (d  I)  fi   
                                        * 
                                        (determinant(n  -  1;r)  matrix-minor(0;i;M))))\mkleeneclose{}\mcdot{}
              THENA  ((RWO  "-2<"  0  THENA  Auto)  THEN  Thin  (-2)  THEN  (Subst'  (n  -  1)  +  1  \msim{}  n  0  THENA  Auto))
              ))

---

Home Index