---

Step * 1 1 of Lemma adjugate-property


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|
BY
{ (HypSubst' (-1) 0
   THEN EqCDA
   THEN Unfold `matrix` 0
   THEN RepeatFor 2 ((FunExt THENA Auto))
   THEN Fold `matrix-ap` 0
   THEN Reduce 0
   THEN AutoSplit) }

---

Latex:

---

Latex:

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
7.  x  =  y
\mvdash{}  |matrix(if  a=y  then  M[x,b]  else  M[a,b])|  =  |M|


By

---

Latex:
(HypSubst'  (-1)  0
  THEN  EqCDA
  THEN  Unfold  `matrix`  0
  THEN  RepeatFor  2  ((FunExt  THENA  Auto))
  THEN  Fold  `matrix-ap`  0
  THEN  Reduce  0
  THEN  AutoSplit)

---

Home Index