Nuprl Definition : ratsub
ratsub(x;y) == ratadd(x;int-rat-mul(-1;y))
Definitions occuring in Statement :
int-rat-mul: int-rat-mul(n;x),
ratadd: ratadd(x;y),
minus: -n,
natural_number: $n
Definitions occuring in definition :
ratadd: ratadd(x;y),
int-rat-mul: int-rat-mul(n;x),
minus: -n,
natural_number: $n
FDL editor aliases :
ratsub
Latex:
ratsub(x;y) == ratadd(x;int-rat-mul(-1;y))
Date html generated:
2019_10_30-AM-09_24_50
Last ObjectModification:
2019_01_11-PM-00_19_12
Theory : reals
Home
Index