Step
*
1
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
{ (Fold `rng_prod` 0 THEN RW CRngNormC 0 THEN Auto) }
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:
(Fold `rng\_prod` 0 THEN RW CRngNormC 0 THEN Auto)
Home
Index