---

Step * of Lemma fps-moebius-inversion

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)].
    g = (f*fps-moebius(eq;r)) ∈ PowerSeries(X;r) supposing f = (g*λb.1) ∈ PowerSeries(X;r) 
  supposing valueall-type(X)
BY
{ xxx(InstLemma `fps-moebius-eq` [] THEN RepeatFor 4 (ParallelLast') THEN Auto)xxx }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. fps-moebius(eq;r) = (1÷λb.1) ∈ PowerSeries(X;r)
6. f : PowerSeries(X;r)
7. g : PowerSeries(X;r)
8. f = (g*λb.1) ∈ PowerSeries(X;r)
⊢ g = (f*fps-moebius(eq;r)) ∈ PowerSeries(X;r)

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[f,g:PowerSeries(X;r)].
        g  =  (f*fps-moebius(eq;r))  supposing  f  =  (g*\mlambda{}b.1) 
    supposing  valueall-type(X)


By

---

Latex:
xxx(InstLemma  `fps-moebius-eq`  []  THEN  RepeatFor  4  (ParallelLast')  THEN  Auto)xxx

---

Home Index