---

Step * 1 of Lemma rng_prod_unroll_hi


1. r : CRng
2. n : ℕ+
3. F : ℕn ⟶ |r|
4. n = 1 ∈ ℤ
⊢ (Π(r) 0 ≤ i < 1. F[i]) = ((Π(r) 0 ≤ i < 1 - 1. F[i]) * F[1 - 1]) ∈ |r|
BY
{ (RepUR ``rng_prod mon_itop`` 0 THEN RepeatFor 2 ((RecUnfold `itop` 0 THEN Reduce 0)) THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  n  :  \mBbbN{}\msupplus{}
3.  F  :  \mBbbN{}n  {}\mrightarrow{}  |r|
4.  n  =  1
\mvdash{}  (\mPi{}(r)  0  \mleq{}  i  <  1.  F[i])  =  ((\mPi{}(r)  0  \mleq{}  i  <  1  -  1.  F[i])  *  F[1  -  1])


By

---

Latex:
(RepUR  ``rng\_prod  mon\_itop``  0  THEN  RepeatFor  2  ((RecUnfold  `itop`  0  THEN  Reduce  0))  THEN  Auto)

---

Home Index