Declare arithmetic with formal variables

edit

In the algebraic way, you can do something like:

sage: R.<x,y> = PolynomialRing(ZZ) ; R
Multivariate Polynomial Ring in x, y over Integer Ring
sage: I = R.ideal(x*y)
sage: I
Ideal (x*y) of Multivariate Polynomial Ring in x, y over Integer Ring
sage: S = R.quotient_ring(I) ; S
Quotient of Multivariate Polynomial Ring in x, y over Integer Ring by the ideal (x*y)
sage: S(3*x*y+x^2+4*y)
xbar^2 + 4*ybar

In the symbolic way, you can do (but it is much less reliable):

sage: var('x y')
(x, y)
sage: assume(x*y==0)
sage: bool(3*x*y+x^2+4*y == x^2+4*y)
True

But is seems not able to decide simplifications by itself:

sage: (3*x*y+x^2+4*y).full_simplify()
x^2 + (3*x + 4)*y

For the orderings, you can also work symbolically:

sage: var('x y')
(x, y)
sage: assume(x<y)
sage: bool(3*x<3*y)
True