---

Step * 2 1 2 2 1 1 1 1 1 of Lemma adjugate-property


1. r : CRng
2. n : ℕ
3. ¬(n = 0 ∈ ℤ)
4. M : Matrix(n;n;r)@i
5. i : ℕn@i
6. d : ℤ
7. b : ℕn@i
8. a : ℕb@i
9. (b - a) ≤ (0 + 1)
⊢ |matrix-minor(a;i;matrix(M[if x=a then b else if x=b then a else x,y]))|
= if isOdd(b - a) then |matrix-minor(b;i;M)| else -r |matrix-minor(b;i;M)| fi 
∈ |r|
BY
{ ((Subst' b - a ~ 1 0 THENA Auto) THEN (Subst' isOdd(1) ~ tt 0 THENA Auto) THEN Reduce 0 THEN EqCDA) }

1
.....subterm..... T:t
3:n
1. r : CRng
2. n : ℕ
3. ¬(n = 0 ∈ ℤ)
4. M : Matrix(n;n;r)@i
5. i : ℕn@i
6. d : ℤ
7. b : ℕn@i
8. a : ℕb@i
9. (b - a) ≤ (0 + 1)
⊢ matrix-minor(a;i;matrix(M[if x=a then b else if x=b then a else x,y])) = matrix-minor(b;i;M) ∈ Matrix(n - 1;n - 1;r)

---

Latex:

---

Latex:

1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  \mneg{}(n  =  0)
4.  M  :  Matrix(n;n;r)@i
5.  i  :  \mBbbN{}n@i
6.  d  :  \mBbbZ{}
7.  b  :  \mBbbN{}n@i
8.  a  :  \mBbbN{}b@i
9.  (b  -  a)  \mleq{}  (0  +  1)
\mvdash{}  |matrix-minor(a;i;matrix(M[if  x=a  then  b  else  if  x=b  then  a  else  x,y]))|
=  if  isOdd(b  -  a)  then  |matrix-minor(b;i;M)|  else  -r  |matrix-minor(b;i;M)|  fi 


By

---

Latex:
((Subst'  b  -  a  \msim{}  1  0  THENA  Auto)  THEN  (Subst'  isOdd(1)  \msim{}  tt  0  THENA  Auto)  THEN  Reduce  0  THEN  EqCDA)

---

Home Index