---

Step * of Lemma poly_int_val_cons_cons-sq

∀n:ℕ. ∀p:polyform(n) List. ∀l:{l:ℤ List| ||l|| = n ∈ ℤ} . ∀a:ℤ. ∀u:polyform(n).
  ([a / l]@[u / p] ~ (l@u * a^||p||) + [a / l]@p)
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}p:polyform(n)  List.  \mforall{}l:\{l:\mBbbZ{}  List|  ||l||  =  n\}  .  \mforall{}a:\mBbbZ{}.  \mforall{}u:polyform(n).
    ([a  /  l]@[u  /  p]  \msim{}  (l@u  *  a\^{}||p||)  +  [a  /  l]@p)


By

---

Latex:
Auto

---

Home Index