---

Step * of Lemma det-mul-row

∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ∀[i:ℕn]. ∀[k:|r|].  (|matrix-mul-row(r;k;i;M)| = (k * |M|) ∈ |r|)
BY
{ (Auto
   THEN Unfold `matrix-det` 0
   THEN (RWO  "rng_times_lsum_l" 0 THENA Auto)
   THEN EqCDA
   THEN (Assert ⌜(Π(r) 0 ≤ i@0 < n. matrix-mul-row(r;k;i;M)[i@0,f i@0]) = (k * (Π(r) 0 ≤ i < n. M[i,f i])) ∈ |r|⌝⋅
   THENM (AutoSplit THEN RepUR ``let`` 0 THEN RWO "-1" 0 THEN Auto)
   )) }

1
.....assertion..... 
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. i : ℕn
5. k : |r|
6. f : ℕn →⟶ ℕn
⊢ (Π(r) 0 ≤ i@0 < n. matrix-mul-row(r;k;i;M)[i@0,f i@0]) = (k * (Π(r) 0 ≤ i < n. M[i,f i])) ∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].  \mforall{}[M:Matrix(n;n;r)].  \mforall{}[i:\mBbbN{}n].  \mforall{}[k:|r|].    (|matrix-mul-row(r;k;i;M)|  =  (k  *  |M|))


By

---

Latex:
(Auto
  THEN  Unfold  `matrix-det`  0
  THEN  (RWO    "rng\_times\_lsum\_l"  0  THENA  Auto)
  THEN  EqCDA
  THEN  (Assert  \mkleeneopen{}(\mPi{}(r)  0 
                                          \mleq{}  i@0 
                                          <  n
                                  matrix-mul-row(r;k;i;M)[i@0,f  i@0])
                              =  (k  *  (\mPi{}(r)  0  \mleq{}  i  <  n.  M[i,f  i]))\mkleeneclose{}\mcdot{}
  THENM  (AutoSplit  THEN  RepUR  ``let``  0  THEN  RWO  "-1"  0  THEN  Auto)
  ))

---

Home Index