Nuprl Definition : int-to-ring
int-to-ring(r;n) == if n <z 0 then -r ((-n) ⋅r 1) else n ⋅r 1 fi
Definitions occuring in Statement :
rng_nat_op: n ⋅r e,
rng_one: 1,
rng_minus: -r,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
apply: f a,
minus: -n,
natural_number: $n
Definitions occuring in definition :
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
natural_number: $n,
apply: f a,
rng_minus: -r,
minus: -n,
rng_nat_op: n ⋅r e,
rng_one: 1
FDL editor aliases :
int-to-ring
Latex:
int-to-ring(r;n) == if n <z 0 then -r ((-n) \mcdot{}r 1) else n \mcdot{}r 1 fi
Date html generated:
2016_05_15-PM-00_26_58
Last ObjectModification:
2015_09_23-AM-06_26_11
Theory : rings_1
Home
Index