---

Step * 4 of Lemma fps-mul-coeff-bag-rep-simple


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. n : ℕ
5. k : ℕn + 1
6. r : CRng
7. f : PowerSeries(X;r)
8. g : PowerSeries(X;r)
9. x : X
10. ∀i:ℕn + 1. ((¬(i = k ∈ ℤ)) ⇒ (f[bag-rep(i;x)] = 0 ∈ |r|))
11. Σ(x∈bag-partitions(eq;bag-rep(n;x))). * f[fst(x)] g[snd(x)]
= (* f[fst(<bag-rep(k;x), bag-rep(n - k;x)>)] g[snd(<bag-rep(k;x), bag-rep(n - k;x)>)])
∈ |r|
⊢ Σ(p∈bag-partitions(eq;bag-rep(n;x))). * (f (fst(p))) (g (snd(p))) = (* (f bag-rep(k;x)) (g bag-rep(n - k;x))) ∈ |r|
BY
{ xxx(RepUR ``fps-coeff`` -1 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  n  :  \mBbbN{}
5.  k  :  \mBbbN{}n  +  1
6.  r  :  CRng
7.  f  :  PowerSeries(X;r)
8.  g  :  PowerSeries(X;r)
9.  x  :  X
10.  \mforall{}i:\mBbbN{}n  +  1.  ((\mneg{}(i  =  k))  {}\mRightarrow{}  (f[bag-rep(i;x)]  =  0))
11.  \mSigma{}(x\mmember{}bag-partitions(eq;bag-rep(n;x))).  *  f[fst(x)]  g[snd(x)]
=  (*  f[fst(<bag-rep(k;x),  bag-rep(n  -  k;x)>)]  g[snd(<bag-rep(k;x),  bag-rep(n  -  k;x)>)])
\mvdash{}  \mSigma{}(p\mmember{}bag-partitions(eq;bag-rep(n;x))).  *  (f  (fst(p)))  (g  (snd(p)))
=  (*  (f  bag-rep(k;x))  (g  bag-rep(n  -  k;x)))


By

---

Latex:
xxx(RepUR  ``fps-coeff``  -1  THEN  Auto)xxx

---

Home Index