---

Step * of Lemma fps-div-property

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)]. ∀[x:|r|].
    (g*(f÷g)) = f ∈ PowerSeries(X;r) supposing (g[{}] * x) = 1 ∈ |r| 
  supposing valueall-type(X)
BY
{ (InstLemma `fps-div-coeff-property` [] THEN Fold `fps-div` (-1) THEN Trivial) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `fps-div-coeff-property`  []  THEN  Fold  `fps-div`  (-1)  THEN  Trivial)

---

Home Index