---

Step * of Lemma dot-product-zero

∀[n:ℕ]. ∀[x:ℝ^n].  (x⋅λi.r0 = r0)
BY
{ (Auto THEN RepUR ``dot-product`` 0) }

1
1. n : ℕ
2. x : ℝ^n
⊢ Σ{(x i) * r0 | 0≤i≤n - 1} = r0

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x:\mBbbR{}\^{}n].    (x\mcdot{}\mlambda{}i.r0  =  r0)


By

---

Latex:
(Auto  THEN  RepUR  ``dot-product``  0)

---

Home Index