---

Step * of Lemma mul_poly-sq

∀[p,q:iMonomial() List].  (mul_ipoly(p;q) ~ mul-ipoly(p;q))
BY
{ InductionOnList }

1
∀[q:iMonomial() List]. (mul_ipoly([];q) ~ mul-ipoly([];q))

2
1. u : iMonomial()
2. v : iMonomial() List
3. ∀[q:iMonomial() List]. (mul_ipoly(v;q) ~ mul-ipoly(v;q))
⊢ ∀[q:iMonomial() List]. (mul_ipoly([u / v];q) ~ mul-ipoly([u / v];q))

---

Latex:

---

Latex:
\mforall{}[p,q:iMonomial()  List].    (mul\_ipoly(p;q)  \msim{}  mul-ipoly(p;q))


By

---

Latex:
InductionOnList

---

Home Index