---

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

.....subterm..... T:t
3:n
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. g[Π(factors(n))]
= Σ(p∈bag-partitions(IntDeq;factors(n))). f[Π(fst(p))] * int-to-ring(r;bag-moebius(IntDeq;snd(p)))
∈ |r|
⊢ Σ i|n. f[i] * int-to-ring(r;int-moebius(n ÷ i))
= Σ(p∈bag-partitions(IntDeq;factors(n))). f[Π(fst(p))] * int-to-ring(r;bag-moebius(IntDeq;snd(p)))
∈ |r|
BY
{ xxx((InstLemma `bag-summation-partitions-primes-general` [⌜r⌝;⌜λ2x y.f[x] 
                                                                       * 
                                                                       int-to-ring(r;bag-moebius(IntDeq;factors(y)))⌝;
       ⌜factors(n)⌝]⋅
       THEN Auto
       )
      THEN Symmetry
      THEN NthHypEq (-1)
      THEN (RepUR ``let`` 0 THEN Fold `int-moebius` 0)
      THEN RepeatFor 5 ((EqCD THEN Auto)))xxx }

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
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.  g[\mPi{}(factors(n))]
=  \mSigma{}(p\mmember{}bag-partitions(IntDeq;factors(n))).  f[\mPi{}(fst(p))]  *  int-to-ring(r;bag-moebius(IntDeq;snd(p)))
\mvdash{}  \mSigma{}  i|n.  f[i]  *  int-to-ring(r;int-moebius(n  \mdiv{}  i))
=  \mSigma{}(p\mmember{}bag-partitions(IntDeq;factors(n))).  f[\mPi{}(fst(p))]  *  int-to-ring(r;bag-moebius(IntDeq;snd(p)))


By

---

Latex:
xxx((InstLemma  `bag-summation-partitions-primes-general`  [\mkleeneopen{}r\mkleeneclose{};
          \mkleeneopen{}\mlambda{}\msubtwo{}x  y.f[x]  *  int-to-ring(r;bag-moebius(IntDeq;factors(y)))\mkleeneclose{};\mkleeneopen{}factors(n)\mkleeneclose{}]\mcdot{}
          THEN  Auto
          )
        THEN  Symmetry
        THEN  NthHypEq  (-1)
        THEN  (RepUR  ``let``  0  THEN  Fold  `int-moebius`  0)
        THEN  RepeatFor  5  ((EqCD  THEN  Auto)))xxx

---

Home Index