### Nuprl 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)`

Proof

Definitions occuring in Statement :  fps-div: `(f÷g)` fps-mul: `(f*g)` fps-coeff: `f[b]` power-series: `PowerSeries(X;r)` empty-bag: `{}` deq: `EqDecider(T)` valueall-type: `valueall-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` infix_ap: `x f y` universe: `Type` equal: `s = t ∈ T` crng: `CRng` rng_one: `1` rng_times: `*` rng_car: `|r|`
Definitions unfolded in proof :  fps-div: `(f÷g)`
Lemmas referenced :  fps-div-coeff-property
Rules used in proof :  cut lemma_by_obid sqequalHypSubstitution sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep hypothesis

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)

Date html generated: 2016_05_15-PM-09_48_49
Last ObjectModification: 2015_12_27-PM-04_40_40

Theory : power!series

Home Index