---

Step * 2 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. g[Π(factors(n))]
= Σ(p∈bag-partitions(IntDeq;factors(n))). f[Π(fst(p))] * int-to-ring(r;bag-moebius(IntDeq;snd(p)))
∈ |r|
⊢ g[n] = Σ i|n. f[i] * int-to-ring(r;int-moebius(n ÷ i)) ∈ |r|
BY
{ xxx(NthHypEq (-1) THEN EqCD THEN Auto)xxx }

1
.....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|

---

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.  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{}  g[n]  =  \mSigma{}  i|n.  f[i]  *  int-to-ring(r;int-moebius(n  \mdiv{}  i))


By

---

Latex:
xxx(NthHypEq  (-1)  THEN  EqCD  THEN  Auto)xxx

---

Home Index