---

Step * 1 1 1 of Lemma det-mul-row


1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. i : ℕn
5. k : |r|
6. f : ℕn →⟶ ℕn
⊢ ((Π 0 ≤ i < i. M[i,f i]) * ((k * M[i,f i]) * (Π i + 1 ≤ i < n. M[i,f i])))
= (k * ((Π 0 ≤ i < i. M[i,f i]) * (M[i,f i] * (Π i + 1 ≤ i < n. M[i,f i]))))
∈ |r|
BY
{ (Subst' * ~ * 0 THENA (RepUR ``mul_mon_of_rng`` 0 THEN 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 < i. M[i,f i]) * ((k * M[i,f i]) * (Π i + 1 ≤ i < n. M[i,f i])))
= (k * ((Π 0 ≤ i < i. M[i,f i]) * (M[i,f i] * (Π i + 1 ≤ i < n. M[i,f i]))))
∈ |r|

---

Latex:

---

Latex:

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{}  0  \mleq{}  i  <  i.  M[i,f  i])  *  ((k  *  M[i,f  i])  *  (\mPi{}  i  +  1  \mleq{}  i  <  n.  M[i,f  i])))
=  (k  *  ((\mPi{}  0  \mleq{}  i  <  i.  M[i,f  i])  *  (M[i,f  i]  *  (\mPi{}  i  +  1  \mleq{}  i  <  n.  M[i,f  i]))))


By

---

Latex:
(Subst'  *  \msim{}  *  0  THENA  (RepUR  ``mul\_mon\_of\_rng``  0  THEN  Auto))

---

Home Index