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. : ℕ+ ⟶ ℤ
2. : ℕ+ ⟶ ℤ
3. ∀n:ℕ+(f[n] = Σ i|n. g[i]  ∈ ℤ)
4. : ℕ+
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