Starting with version 1.2, a new division algorithm has been implemented in rings with inverses, where the monomials can involve negative exponents, and hence do not form a well-ordered set. The ring should have a monomial ordering whose first test involves at least one weight vector, explicitly, or perhaps implicitly, as with GRevLex. The algorithm will work when dividing by a polynomial that is monic in the sense that its lead monomial has coefficient 1, and all other terms have smaller weight, where the weight is computed with respect to just the first weight vector. When we say the algorithm works, we mean: (1) that it terminates; and (2) that the remainder is zero if and only if the denominator divides the numerator.
Define the length of a nonzero ring element to be the weight of the first term minus the weight of the last term. The length is greater than or equal to 0, because the terms in a sorted polynomial are decreasing in weight.
We refuse to start dividing unless the denominator is monic in the sense defined above. When dividing, we keep subtracting monomial multiples of the denominator from the numerator to eliminate the lead term of the numerator, which is always possible because the ring contains the reciprocals of its variables. We stop when we get a remainder whose length is strictly less than the length of the denominator.
This algorithm works because, in an integral domain, the length of a product is the sum of the lengths of the factors. Thus the remainder, if it is not zero, can not be a multiple of the denominator.
This will be good enough for applications to Hilbert series, because in our degrees rings, the denominator of a Hilbert series will be a product of terms 1-T, where T is a monomial of strictly negative weight. That's because the weight vector is minus the heft vector of the original ring, and T is the monomial constructed from the degree vector of one of the variables in the original ring. Note that any divisor of such a product will also be 1 plus terms of negative weight.