---

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


1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
4. i : ℕn
5. row : ℕn ⟶ |r|
6. f : ℕn →⟶ ℕn
⊢ ((Π(r) 0 ≤ i < i. M[i,f i]) * (((row (f i)) +r M[i,f i]) * (Π(r) i + 1 ≤ i < n. M[i,f i])))
= (((Π(r) 0 ≤ i < i. M[i,f i]) * ((row (f i)) * (Π(r) i + 1 ≤ i < n. M[i,f i]))) 
   +r 
   ((Π(r) 0 ≤ i < i. M[i,f i]) * (M[i,f i] * (Π(r) i + 1 ≤ i < n. M[i,f i]))))
∈ |r|
BY
{ (RW RngNormC 0 THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  M  :  Matrix(n;n;r)
4.  i  :  \mBbbN{}n
5.  row  :  \mBbbN{}n  {}\mrightarrow{}  |r|
6.  f  :  \mBbbN{}n  \mrightarrow{}{}\mrightarrow{}  \mBbbN{}n
\mvdash{}  ((\mPi{}(r)  0  \mleq{}  i  <  i.  M[i,f  i])  *  (((row  (f  i))  +r  M[i,f  i])  *  (\mPi{}(r)  i  +  1  \mleq{}  i  <  n.  M[i,f  i])))
=  (((\mPi{}(r)  0  \mleq{}  i  <  i.  M[i,f  i])  *  ((row  (f  i))  *  (\mPi{}(r)  i  +  1  \mleq{}  i  <  n.  M[i,f  i]))) 
      +r 
      ((\mPi{}(r)  0  \mleq{}  i  <  i.  M[i,f  i])  *  (M[i,f  i]  *  (\mPi{}(r)  i  +  1  \mleq{}  i  <  n.  M[i,f  i]))))


By

---

Latex:
(RW  RngNormC  0  THEN  Auto)

---

Home Index