---

Step * of Lemma int-prod-factor

∀[n:ℕ]. ∀[f,g:ℕn ⟶ ℤ].  (Π(f[x] * g[x] | x < n) = (Π(f[x] | x < n) * Π(g[x] | x < n)) ∈ ℤ)
BY
{ (PrimrecInductionOn `n'⋅ THEN Auto THEN RWO "-3" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f,g:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].    (\mPi{}(f[x]  *  g[x]  |  x  <  n)  =  (\mPi{}(f[x]  |  x  <  n)  *  \mPi{}(g[x]  |  x  <  n)))


By

---

Latex:
(PrimrecInductionOn  `n'\mcdot{}  THEN  Auto  THEN  RWO  "-3"  0  THEN  Auto)

---

Home Index