---

Step * of Lemma int-moebius-inversion-general

∀[r:CRng]. ∀[f,g:ℕ+ ⟶ |r|].
  ∀n:ℕ+. (g[n] = Σ i|n. f[i] * int-to-ring(r;int-moebius(n ÷ i)) ∈ |r|) supposing ∀n:ℕ+. (f[n] = Σ i|n. g[i] ∈ |r|)
BY
{ xxx(Auto
      THEN (Assert IntDeq ∈ EqDecider(Prime) BY
                  (DoSubsume THEN Auto THEN BLemma `strong-subtype-deq-subtype` THEN Auto))
      THEN (InstLemma `bag-moebius-inversion` [⌜Prime⌝;⌜IntDeq⌝;⌜r⌝]⋅ THENA Auto)
      THEN ((InstHyp [⌜λb.f[Π(b)]⌝;⌜λb.g[Π(b)]⌝;⌜factors(n)⌝] (-1)⋅ THENM Reduce (-1)) THENA (Reduce 0 THEN 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)
⊢ f[Π(b)] = Σ(s∈sub-bags(IntDeq;b)). g[Π(s)] ∈ |r|

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

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[f,g:\mBbbN{}\msupplus{}  {}\mrightarrow{}  |r|].
    \mforall{}n:\mBbbN{}\msupplus{}.  (g[n]  =  \mSigma{}  i|n.  f[i]  *  int-to-ring(r;int-moebius(n  \mdiv{}  i))) 
    supposing  \mforall{}n:\mBbbN{}\msupplus{}.  (f[n]  =  \mSigma{}  i|n.  g[i])


By

---

Latex:
xxx(Auto
        THEN  (Assert  IntDeq  \mmember{}  EqDecider(Prime)  BY
                                (DoSubsume  THEN  Auto  THEN  BLemma  `strong-subtype-deq-subtype`  THEN  Auto))
        THEN  (InstLemma  `bag-moebius-inversion`  [\mkleeneopen{}Prime\mkleeneclose{};\mkleeneopen{}IntDeq\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  ((InstHyp  [\mkleeneopen{}\mlambda{}b.f[\mPi{}(b)]\mkleeneclose{};\mkleeneopen{}\mlambda{}b.g[\mPi{}(b)]\mkleeneclose{};\mkleeneopen{}factors(n)\mkleeneclose{}]  (-1)\mcdot{}  THENM  Reduce  (-1))
                    THENA  (Reduce  0  THEN  Auto)
                    ))xxx

---

Home Index