---

Step * of Lemma polynom-equal-iff

∀[n:ℕ]. ∀[p,q:polynom(n)].  uiff(p = q ∈ polynom(n);∀l:{l:ℤ List| ||l|| = n ∈ ℤ} . (p@l = q@l ∈ ℤ))
BY
{ Auto }

1
1. n : ℕ
2. p : polynom(n)
3. q : polynom(n)
4. ∀l:{l:ℤ List| ||l|| = n ∈ ℤ} . (p@l = q@l ∈ ℤ)
⊢ p = q ∈ polynom(n)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[p,q:polynom(n)].    uiff(p  =  q;\mforall{}l:\{l:\mBbbZ{}  List|  ||l||  =  n\}  .  (p@l  =  q@l))


By

---

Latex:
Auto

---

Home Index