### Nuprl Definition : pa-inv

`pa-inv(p;x) ==`
`  let n,a = x `
`  in if (n =z 0)`
`     then eval k = mu(λi.(¬b(a (i + 1) =z 0))) in`
`          let j,b = p-unitize(p;a;k + 1) `
`          in <j, p-inv(p;b)>`
`     else <0, p^n(p) * p-inv(p;a)>`
`     fi `

Definitions occuring in Statement :  p-unitize: `p-unitize(p;a;n)` p-inv: `p-inv(p;a)` p-int: `k(p)` p-mul: `x * y` fastexp: `i^n` mu: `mu(f)` callbyvalue: callbyvalue bnot: `¬bb` ifthenelse: `if b then t else f fi ` eq_int: `(i =z j)` apply: `f a` lambda: `λx.A[x]` spread: spread def pair: `<a, b>` add: `n + m` natural_number: `\$n`
Definitions occuring in definition :  ifthenelse: `if b then t else f fi ` callbyvalue: callbyvalue mu: `mu(f)` lambda: `λx.A[x]` bnot: `¬bb` eq_int: `(i =z j)` apply: `f a` spread: spread def p-unitize: `p-unitize(p;a;n)` add: `n + m` pair: `<a, b>` natural_number: `\$n` p-mul: `x * y` p-int: `k(p)` fastexp: `i^n` p-inv: `p-inv(p;a)`
FDL editor aliases :  pa-inv

Latex:
pa-inv(p;x)  ==
let  n,a  =  x
in  if  (n  =\msubz{}  0)
then  eval  k  =  mu(\mlambda{}i.(\mneg{}\msubb{}(a  (i  +  1)  =\msubz{}  0)))  in
let  j,b  =  p-unitize(p;a;k  +  1)
in  <j,  p-inv(p;b)>
else  ɘ,  p\^{}n(p)  *  p-inv(p;a)>
fi

Date html generated: 2018_05_21-PM-03_28_41
Last ObjectModification: 2018_02_05-AM-11_17_07

Theory : rings_1

Home Index