Nuprl Definition : rpoly-deriv
rpoly-deriv(n;a;x) == if (n =z 0) then r0 else (Σi≤n - 1. poly-deriv(a)_i * x^i) fi
Definitions occuring in Statement :
poly-deriv: poly-deriv(a),
rpolynomial: (Σi≤n. a_i * x^i),
int-to-real: r(n),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
int-to-real: r(n),
rpolynomial: (Σi≤n. a_i * x^i),
subtract: n - m,
natural_number: $n,
poly-deriv: poly-deriv(a)
FDL editor aliases :
rpoly-deriv
Latex:
rpoly-deriv(n;a;x) == if (n =\msubz{} 0) then r0 else (\mSigma{}i\mleq{}n - 1. poly-deriv(a)\_i * x\^{}i) fi
Date html generated:
2016_05_18-AM-10_09_25
Last ObjectModification:
2015_09_23-AM-09_15_00
Theory : reals
Home
Index