---

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

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[n:ℕ]. ∀[k:ℕn + 1]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)]. ∀[x:X].
    (f*g)[bag-rep(n;x)] = (* f[bag-rep(k;x)] g[bag-rep(n - k;x)]) ∈ |r| 
    supposing ∀i:ℕn + 1. ((¬(i = k ∈ ℤ)) ⇒ (f[bag-rep(i;x)] = 0 ∈ |r|)) 
  supposing valueall-type(X)
BY
{ xxx(Auto
      THEN RepUR ``fps-mul fps-coeff`` 0
      THEN (InstLemma `bag-summation-single-non-zero-no-repeats` 
             [⌜bag(X) × bag(X)⌝;⌜|r|⌝;⌜product-deq(bag(X);bag(X);bag-deq(eq);bag-deq(eq))⌝
             ;⌜+r⌝;⌜0⌝
             ; ⌜bag-partitions(eq;bag-rep(n;x))⌝
             ; ⌜λ2p.* f[fst(p)] g[snd(p)]⌝
             ; ⌜<bag-rep(k;x), bag-rep(n - k;x)>⌝]⋅
            THENA (Auto THEN Try (RepeatFor 2 (((D 0 THEN Reduce 0) THEN Auto)⋅)))
            ))xxx }

1
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@0 : bag(X) × bag(X)
12. x@0 ↓∈ bag-partitions(eq;bag-rep(n;x))
⊢ (x@0 = <bag-rep(k;x), bag-rep(n - k;x)> ∈ (bag(X) × bag(X))) ∨ ((* f[fst(x@0)] g[snd(x@0)]) = 0 ∈ |r|)

2
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|))
⊢ bag-no-repeats(bag(X) × bag(X);bag-partitions(eq;bag-rep(n;x)))

3
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. bag-no-repeats(bag(X) × bag(X);bag-partitions(eq;bag-rep(n;x)))
⊢ <bag-rep(k;x), bag-rep(n - k;x)> ↓∈ bag-partitions(eq;bag-rep(n;x))

4
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|

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[n:\mBbbN{}].  \mforall{}[k:\mBbbN{}n  +  1].  \mforall{}[r:CRng].  \mforall{}[f,g:PowerSeries(X;r)].  \mforall{}[x:X].
        (f*g)[bag-rep(n;x)]  =  (*  f[bag-rep(k;x)]  g[bag-rep(n  -  k;x)]) 
        supposing  \mforall{}i:\mBbbN{}n  +  1.  ((\mneg{}(i  =  k))  {}\mRightarrow{}  (f[bag-rep(i;x)]  =  0)) 
    supposing  valueall-type(X)


By

---

Latex:
xxx(Auto
        THEN  RepUR  ``fps-mul  fps-coeff``  0
        THEN  (InstLemma  `bag-summation-single-non-zero-no-repeats` 
                      [\mkleeneopen{}bag(X)  \mtimes{}  bag(X)\mkleeneclose{};\mkleeneopen{}|r|\mkleeneclose{};\mkleeneopen{}product-deq(bag(X);bag(X);bag-deq(eq);bag-deq(eq))\mkleeneclose{}
                      ;\mkleeneopen{}+r\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}
                      ;  \mkleeneopen{}bag-partitions(eq;bag-rep(n;x))\mkleeneclose{}
                      ;  \mkleeneopen{}\mlambda{}\msubtwo{}p.*  f[fst(p)]  g[snd(p)]\mkleeneclose{}
                      ;  \mkleeneopen{}<bag-rep(k;x),  bag-rep(n  -  k;x)>\mkleeneclose{}]\mcdot{}
                    THENA  (Auto  THEN  Try  (RepeatFor  2  (((D  0  THEN  Reduce  0)  THEN  Auto)\mcdot{})))
                    ))xxx

---

Home Index