---

Step * 1 of Lemma det-mul-row

.....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|
BY
{ (Unfold `rng_prod` 0 THEN (RWH (LemmaWithC [`b',i] `mon_itop_split_el`) 0 THENA Auto)) }

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

---

Latex:

---

Latex:
.....assertion..... 
1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  M  :  Matrix(n;n;r)
4.  i  :  \mBbbN{}n
5.  k  :  |r|
6.  f  :  \mBbbN{}n  \mrightarrow{}{}\mrightarrow{}  \mBbbN{}n
\mvdash{}  (\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]))


By

---

Latex:
(Unfold  `rng\_prod`  0  THEN  (RWH  (LemmaWithC  [`b',i]  `mon\_itop\_split\_el`)  0  THENA  Auto))

---

Home Index