---

Step * 1 of Lemma adjugate-property

.....assertion..... 
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. ¬(n = 0 ∈ ℤ)
5. x : ℕn@i
6. y : ℕn@i
⊢ |matrix(if a=y then M[x,b] else M[a,b])| = (|M| * if x=y then 1 else 0) ∈ |r|
BY
{ ((Decide ⌜x = y ∈ ℤ⌝⋅ THENA Auto) THEN (Reduce 0 THENA Auto) THEN (RW RngNormC 0 THENA Auto)) }

1
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. ¬(n = 0 ∈ ℤ)
5. x : ℕn@i
6. y : ℕn@i
7. x = y ∈ ℤ
⊢ |matrix(if a=y then M[x,b] else M[a,b])| = |M| ∈ |r|

2
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. ¬(n = 0 ∈ ℤ)
5. x : ℕn@i
6. y : ℕn@i
7. ¬(x = y ∈ ℤ)
⊢ |matrix(if a=y then M[x,b] else M[a,b])| = 0 ∈ |r|

---

Latex:

---

Latex:
.....assertion..... 
1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  M  :  Matrix(n;n;r)
4.  \mneg{}(n  =  0)
5.  x  :  \mBbbN{}n@i
6.  y  :  \mBbbN{}n@i
\mvdash{}  |matrix(if  a=y  then  M[x,b]  else  M[a,b])|  =  (|M|  *  if  x=y  then  1  else  0)


By

---

Latex:
((Decide  \mkleeneopen{}x  =  y\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (Reduce  0  THENA  Auto)  THEN  (RW  RngNormC  0  THENA  Auto))

---

Home Index