---

Step * of Lemma int-moebius-inversion

∀[f,g:ℕ+ ⟶ ℤ].  ∀n:ℕ+. (g[n] = Σ i|n. f[i] * int-moebius(n ÷ i)  ∈ ℤ) supposing ∀n:ℕ+. (f[n] = Σ i|n. g[i]  ∈ ℤ)
BY
{ xxx(Auto
      THEN (InstLemma `int-moebius-inversion-general` [⌜ℤ-rng⌝;⌜f⌝;⌜g⌝;⌜n⌝]⋅ THENA Auto)
      THEN All (RWO "gen-divisors-sum-int-ring")
      THEN Auto)xxx }

1
1. f : ℕ+ ⟶ ℤ
2. g : ℕ+ ⟶ ℤ
3. ∀n:ℕ+. (f[n] = Σ i|n. g[i]  ∈ ℤ)
4. n : ℕ+
5. g[n] = Σ i|n. f[i] * int-to-ring(ℤ-rng;int-moebius(n ÷ i))  ∈ |ℤ-rng|
⊢ g[n] = Σ i|n. f[i] * int-moebius(n ÷ i)  ∈ ℤ

---

Latex:

---

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


By

---

Latex:
xxx(Auto
        THEN  (InstLemma  `int-moebius-inversion-general`  [\mkleeneopen{}\mBbbZ{}-rng\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  All  (RWO  "gen-divisors-sum-int-ring")
        THEN  Auto)xxx

---

Home Index