---

Step * of Lemma expand-det-by-column

∀[n:ℕ]. ∀[j:ℕn]. ∀[r:CRng]. ∀[M:Matrix(n;n;r)].
  (|M| = (Σ(r) 0 ≤ i < n. if isEven(i + j) then M[i,j] else -r M[i,j] fi  * |matrix-minor(i;j;M)|) ∈ |r|)
BY
{ (Auto
   THEN (Assert (adj(M)*M)[j,j] = |M|*I[j,j] ∈ |r| BY
               (EqCDA THEN Auto))
   THEN (RepUR ``matrix-scalar-mul identity-matrix`` -1 THEN (RW  RngNormC (-1) THENA Auto))
   THEN NthHypEqTrans (-1)
   THEN RepUR ``matrix-times adjugate`` 0
   THEN EqCDA
   THEN (Subst' j + i ~ i + j 0 THENA Auto)
   THEN AutoSplit
   THEN RW RngNormC 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[j:\mBbbN{}n].  \mforall{}[r:CRng].  \mforall{}[M:Matrix(n;n;r)].
    (|M|  =  (\mSigma{}(r)  0  \mleq{}  i  <  n.  if  isEven(i  +  j)  then  M[i,j]  else  -r  M[i,j]  fi    *  |matrix-minor(i;j;M)|))


By

---

Latex:
(Auto
  THEN  (Assert  (adj(M)*M)[j,j]  =  |M|*I[j,j]  BY
                          (EqCDA  THEN  Auto))
  THEN  (RepUR  ``matrix-scalar-mul  identity-matrix``  -1  THEN  (RW    RngNormC  (-1)  THENA  Auto))
  THEN  NthHypEqTrans  (-1)
  THEN  RepUR  ``matrix-times  adjugate``  0
  THEN  EqCDA
  THEN  (Subst'  j  +  i  \msim{}  i  +  j  0  THENA  Auto)
  THEN  AutoSplit
  THEN  RW  RngNormC  0
  THEN  Auto)

---

Home Index