Nuprl Definition : rat-term-eq
rat-term-eq(r1;r2) ==
let p1,q1 = rat_term_to_ipolys(r1)
in let p2,q2 = rat_term_to_ipolys(r2)
in null(add-ipoly(mul-ipoly(p1;q2);mul-ipoly(minus-poly(p2);q1)))
Definitions occuring in Statement :
rat_term_to_ipolys: rat_term_to_ipolys(t),
mul-ipoly: mul-ipoly(p;q),
minus-poly: minus-poly(p),
add-ipoly: add-ipoly(p;q),
null: null(as),
spread: spread def
Definitions occuring in definition :
spread: spread def,
rat_term_to_ipolys: rat_term_to_ipolys(t),
null: null(as),
add-ipoly: add-ipoly(p;q),
mul-ipoly: mul-ipoly(p;q),
minus-poly: minus-poly(p)
FDL editor aliases :
rat-term-eq
Latex:
rat-term-eq(r1;r2) ==
let p1,q1 = rat\_term\_to\_ipolys(r1)
in let p2,q2 = rat\_term\_to\_ipolys(r2)
in null(add-ipoly(mul-ipoly(p1;q2);mul-ipoly(minus-poly(p2);q1)))
Date html generated:
2019_10_29-AM-09_53_42
Last ObjectModification:
2019_04_01-PM-01_03_29
Theory : reals
Home
Index