---

Step * of Lemma ml-int-vec-mul-sq

∀[a:ℤ]. ∀[as:ℤ List].  (ml-int-vec-mul(a;as) ~ a * as)
BY
{ ((Unfold `ml-int-vec-mul` 0 THEN Auto) THEN RWO "ml-map-sq" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[as:\mBbbZ{}  List].    (ml-int-vec-mul(a;as)  \msim{}  a  *  as)


By

---

Latex:
((Unfold  `ml-int-vec-mul`  0  THEN  Auto)  THEN  RWO  "ml-map-sq"  0  THEN  Auto)

---

Home Index