---

Step * 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)
⊢ f[Π(b)] = Σ(s∈sub-bags(IntDeq;b)). g[Π(s)] ∈ |r|
BY
{ xxx(RWO "4" 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∈sub-bags(IntDeq;b)). g[Π(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{}  f[\mPi{}(b)]  =  \mSigma{}(s\mmember{}sub-bags(IntDeq;b)).  g[\mPi{}(s)]


By

---

Latex:
xxx(RWO  "4"  0  THENA  Auto)xxx

---

Home Index