Nuprl Definition : p-unitize
p-unitize(p;a;n) ==  eval k = greatest-p-zero(n;a) in <k, if k=0 then a else p-shift(p;a;k)>
Definitions occuring in Statement : 
greatest-p-zero: greatest-p-zero(n;a)
, 
p-shift: p-shift(p;a;k)
, 
callbyvalue: callbyvalue, 
int_eq: if a=b then c else d
, 
pair: <a, b>
, 
natural_number: $n
Definitions occuring in definition : 
callbyvalue: callbyvalue, 
greatest-p-zero: greatest-p-zero(n;a)
, 
pair: <a, b>
, 
int_eq: if a=b then c else d
, 
natural_number: $n
, 
p-shift: p-shift(p;a;k)
FDL editor aliases : 
p-unitize
Latex:
p-unitize(p;a;n)  ==    eval  k  =  greatest-p-zero(n;a)  in  <k,  if  k=0  then  a  else  p-shift(p;a;k)>
Date html generated:
2018_05_21-PM-03_22_23
Last ObjectModification:
2018_02_01-AM-10_37_41
Theory : rings_1
Home
Index