---

Step * 1 1 1 of Lemma int-moebius-inversion-general


1. r : CRng
2. f : ℕ+ ⟶ |r|
3. g : ℕ+ ⟶ |r|
4. ∀n:ℕ+. (f[n] = Σ i|n. g[i] ∈ |r|)
5. n : ℕ+
6. IntDeq ∈ EqDecider(Prime)
7. ∀[f,g:bag(Prime) ⟶ |r|].
     ∀b:bag(Prime)
       ((g b) = Σ(p∈bag-partitions(IntDeq;b)). (f (fst(p))) * int-to-ring(r;bag-moebius(IntDeq;snd(p))) ∈ |r|) 
     supposing ∀b:bag(Prime). ((f b) = Σ(s∈sub-bags(IntDeq;b)). g s ∈ |r|)
8. b : bag(Prime)
⊢ Σ i|Π(b). g[i] = Σ(s∈bag-partitions(IntDeq;b)). g[Π(fst(s))] ∈ |r|
BY
{ xxx(InstLemma `bag-summation-partitions-primes-general` [⌜r⌝;⌜⌜λ2x y.g[x]⌝⌝]⋅
      THEN Auto
      THEN RWO "-1" 0
      THEN Auto)xxx }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  f  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  |r|
3.  g  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  |r|
4.  \mforall{}n:\mBbbN{}\msupplus{}.  (f[n]  =  \mSigma{}  i|n.  g[i])
5.  n  :  \mBbbN{}\msupplus{}
6.  IntDeq  \mmember{}  EqDecider(Prime)
7.  \mforall{}[f,g:bag(Prime)  {}\mrightarrow{}  |r|].
          \mforall{}b:bag(Prime)
              ((g  b)
              =  \mSigma{}(p\mmember{}bag-partitions(IntDeq;b)).  (f  (fst(p)))  *  int-to-ring(r;bag-moebius(IntDeq;snd(p)))) 
          supposing  \mforall{}b:bag(Prime).  ((f  b)  =  \mSigma{}(s\mmember{}sub-bags(IntDeq;b)).  g  s)
8.  b  :  bag(Prime)
\mvdash{}  \mSigma{}  i|\mPi{}(b).  g[i]  =  \mSigma{}(s\mmember{}bag-partitions(IntDeq;b)).  g[\mPi{}(fst(s))]


By

---

Latex:
xxx(InstLemma  `bag-summation-partitions-primes-general`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}\mkleeneopen{}\mlambda{}\msubtwo{}x  y.g[x]\mkleeneclose{}\mkleeneclose{}]\mcdot{}
        THEN  Auto
        THEN  RWO  "-1"  0
        THEN  Auto)xxx

---

Home Index