Elimination over skew fields

Over a commutative field there is a process known as the elimination of quantifiers, which is very useful. The simplest instance is provided by the resultant of two polynomials, whose vanishing is a criterion for the two polynomials to have a common zero. More precisely, given two polynomials f = ∑a_ixⁱ , g = ∑b_jx^j over a field k, there exists a polynomial R(a, b) in the coefficients a_i , b_j such that R(a, b) = 0 if and only if f and g have a common zero in some extension field of k. Here we must be careful to allow ∞ as a possible zero; alternatively we could replace x by a projective coordinate.