Nuprl Definition : rcp
(a x b) == λi.[((a 1) * (b 2)) - (a 2) * (b 1); ((a 2) * (b 0)) - (a 0) * (b 2); ((a 0) * (b 1)) - (a 1) * (b 0)][i]
Definitions occuring in Statement :
rsub: x - y,
rmul: a * b,
select: L[n],
cons: [a / b],
nil: [],
apply: f a,
lambda: λx.A[x],
natural_number: $n
Definitions occuring in definition :
nil: [],
natural_number: $n,
apply: f a,
rmul: a * b,
rsub: x - y,
cons: [a / b],
select: L[n],
lambda: λx.A[x]
FDL editor aliases :
rcp
Latex:
(a x b) ==
\mlambda{}i.[((a 1) * (b 2)) - (a 2) * (b 1);
((a 2) * (b 0)) - (a 0) * (b 2);
((a 0) * (b 1)) - (a 1) * (b 0)][i]
Date html generated:
2018_05_22-PM-02_39_01
Last ObjectModification:
2018_05_09-PM-00_50_31
Theory : reals
Home
Index