---

Step * of Lemma l_sum-mul-left

∀[L:ℤ List]. ∀[m:ℤ].  (m * l_sum(L) ~ l_sum(map(λx.(m * x);L)))
BY
{ (InductionOnList THEN Reduce 0 THEN Auto THEN RWO "-2<" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L:\mBbbZ{}  List].  \mforall{}[m:\mBbbZ{}].    (m  *  l\_sum(L)  \msim{}  l\_sum(map(\mlambda{}x.(m  *  x);L)))


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto  THEN  RWO  "-2<"  0  THEN  Auto)

---

Home Index