---

Step * of Lemma q-linear-base

∀[X:ℕ ⟶ ℚ]. ∀[y:ℚ List].  (q-linear(0;j.X[j];y) = X[0] ∈ ℚ)
BY
{ xxx(Auto THEN Unfold `q-linear` 0 THEN (RWO "sum_unroll_base_q" 0 THENA Auto))xxx }

1
1. X : ℕ ⟶ ℚ
2. y : ℚ List
⊢ (X[0] + 0) = X[0] ∈ ℚ

---

Latex:

---

Latex:
\mforall{}[X:\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}].  \mforall{}[y:\mBbbQ{}  List].    (q-linear(0;j.X[j];y)  =  X[0])


By

---

Latex:
xxx(Auto  THEN  Unfold  `q-linear`  0  THEN  (RWO  "sum\_unroll\_base\_q"  0  THENA  Auto))xxx

---

Home Index