---

Step * of Lemma rpolynomial-rmul

∀[n:ℕ]. ∀[a:ℕn + 1 ⟶ ℝ]. ∀[x,b:ℝ].  (((Σi≤n. a_i * x^i) * b) = (Σi≤n. λi.((a i) * b)_i * x^i))
BY
{ (InstLemma `rmul-rpolynomial` [] THEN RepeatFor 4 (ParallelLast')) }

1
1. [n] : ℕ
2. [a] : ℕn + 1 ⟶ ℝ
3. [x] : ℝ
4. [b] : ℝ
5. (b * (Σi≤n. a_i * x^i)) = (Σi≤n. λi.(b * (a i))_i * x^i)
⊢ ((Σi≤n. a_i * x^i) * b) = (Σi≤n. λi.((a i) * b)_i * x^i)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[a:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[x,b:\mBbbR{}].    (((\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i)  *  b)  =  (\mSigma{}i\mleq{}n.  \mlambda{}i.((a  i)  *  b)\_i  *  x\^{}i))


By

---

Latex:
(InstLemma  `rmul-rpolynomial`  []  THEN  RepeatFor  4  (ParallelLast'))

---

Home Index