---

Step * of Lemma fps-moebius-eq

∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng].  (fps-moebius(eq;r) = (1÷λb.1) ∈ PowerSeries(X;r)) supposing valueall-type(X)
BY
{ TACTIC:(Auto
          THEN RepUR ``fps-moebius power-series fps-div`` 0
          THEN (EqCD THENA Auto)
          THEN (CallByValueReduce 0 THENA Auto)) }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. b : bag(X)
⊢ int-to-ring(r;bag-moebius(eq;b)) = fps-div-coeff(eq;r;1;λb.1;1;b) ∈ |r|

---

Latex:

---

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


By

---

Latex:
TACTIC:(Auto
                THEN  RepUR  ``fps-moebius  power-series  fps-div``  0
                THEN  (EqCD  THENA  Auto)
                THEN  (CallByValueReduce  0  THENA  Auto))

---

Home Index