---

Step * 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∈sub-bags(IntDeq;b)). g[Π(s)] ∈ |r|
BY
{ xxx(Unfold `sub-bags` 0 THEN ((RWO "bag-summation-map" 0 THENM Reduce 0) THENA Auto))xxx }

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

---

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{}sub-bags(IntDeq;b)).  g[\mPi{}(s)]


By

---

Latex:
xxx(Unfold  `sub-bags`  0  THEN  ((RWO  "bag-summation-map"  0  THENM  Reduce  0)  THENA  Auto))xxx

---

Home Index