---

Step * 1 of Lemma int-moebius-inversion


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)  ∈ ℤ
BY
{ xxx(Reduce (-1) THEN HypSubst' (-1) 0 THEN EqCD THEN Auto)xxx }

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
2.  g  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  \mforall{}n:\mBbbN{}\msupplus{}.  (f[n]  =  \mSigma{}  i|n.  g[i]  )
4.  n  :  \mBbbN{}\msupplus{}
5.  g[n]  =  \mSigma{}  i|n.  f[i]  *  int-to-ring(\mBbbZ{}-rng;int-moebius(n  \mdiv{}  i)) 
\mvdash{}  g[n]  =  \mSigma{}  i|n.  f[i]  *  int-moebius(n  \mdiv{}  i) 


By

---

Latex:
xxx(Reduce  (-1)  THEN  HypSubst'  (-1)  0  THEN  EqCD  THEN  Auto)xxx

---

Home Index