---

Step * 2 1 1 1 of Lemma adjugate-property


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|
BY
{ ((Subst' (n - 1) + 1 ~ n 0 THENA Auto) THEN RepeatFor 2 (EqCDA) THEN Subst' i + 0 ~ i 0 THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  \mneg{}n  <  1
4.  \mneg{}(n  =  0)
5.  M  :  Matrix(n;n;r)@i
\mvdash{}  (\mSigma{}(r)  0 
                \mleq{}  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)))
=  (\mSigma{}(r)  0 
                \mleq{}  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)))


By

---

Latex:
((Subst'  (n  -  1)  +  1  \msim{}  n  0  THENA  Auto)  THEN  RepeatFor  2  (EqCDA)  THEN  Subst'  i  +  0  \msim{}  i  0  THEN  Auto)

---

Home Index