---

Step * of Lemma adjugate-property

∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)].  ((M*adj(M)) = |M|*I ∈ Matrix(n;n;r))
BY
{ (Auto
   THEN (CaseNat 0 `n'
         THENL [(Unfold `matrix` 0 THEN FunExt THEN Auto)
               ; (Unfolds ``matrix-times matrix-scalar-mul`` 0
                  THEN EqCDA
                  THEN RepUR ``identity-matrix adjugate`` 0
                  THEN Assert ⌜|matrix(if a=y then M[x,b] else M[a,b])| = (|M| * if x=y then 1 else 0) ∈ |r|⌝⋅)]
        )
   ) }

1
.....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|

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

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].  \mforall{}[M:Matrix(n;n;r)].    ((M*adj(M))  =  |M|*I)


By

---

Latex:
(Auto
  THEN  (CaseNat  0  `n'
              THENL  [(Unfold  `matrix`  0  THEN  FunExt  THEN  Auto)
                          ;  (Unfolds  ``matrix-times  matrix-scalar-mul``  0
                                THEN  EqCDA
                                THEN  RepUR  ``identity-matrix  adjugate``  0
                                THEN  Assert 
                                \mkleeneopen{}|matrix(if  a=y  then  M[x,b]  else  M[a,b])|  =  (|M|  *  if  x=y  then  1  else  0)\mkleeneclose{}\mcdot{})]
            )
  )

---

Home Index