---

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


1. r : CRng
2. n : ℤ
3. ¬n < 1
4. 0 < n
5. d : det-fun(r;n)
6. M : Matrix(n;n;r)
7. (d M) = (Σ(r) 0 ≤ i < n. M[0,i] * (d matrix(if x=0 then if y=i then 1 else 0 else M[x,y]))) ∈ |r|
8. i : ℕn
9. j : ℤ
10. x : ℕn
11. y : ℕn
12. y ≠ i
13. ¬(x = 0 ∈ ℤ)
14. 0 < x
⊢ M[x,y]
= if (y) < (i)  then matrix-minor(0;i;M)[x - 1,y]  else if (i) < (y)  then matrix-minor(0;i;M)[x - 1,y - 1]  else 0
∈ |r|
BY
{ (RepUR ``matrix-minor mx matrix-ap`` 0 THEN Fold `matrix-ap` 0 THEN AutoSplit) }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  n  :  \mBbbZ{}
3.  \mneg{}n  <  1
4.  0  <  n
5.  d  :  det-fun(r;n)
6.  M  :  Matrix(n;n;r)
7.  (d  M)  =  (\mSigma{}(r)  0  \mleq{}  i  <  n.  M[0,i]  *  (d  matrix(if  x=0  then  if  y=i  then  1  else  0  else  M[x,y])))
8.  i  :  \mBbbN{}n
9.  j  :  \mBbbZ{}
10.  x  :  \mBbbN{}n
11.  y  :  \mBbbN{}n
12.  y  \mneq{}  i
13.  \mneg{}(x  =  0)
14.  0  <  x
\mvdash{}  M[x,y]
=  if  (y)  <  (i)
          then  matrix-minor(0;i;M)[x  -  1,y]
          else  if  (i)  <  (y)    then  matrix-minor(0;i;M)[x  -  1,y  -  1]    else  0


By

---

Latex:
(RepUR  ``matrix-minor  mx  matrix-ap``  0  THEN  Fold  `matrix-ap`  0  THEN  AutoSplit)

---

Home Index