Multivariate polynomial, where σ is the index set of the variables and α is the coefficient ring
monomial s a is the monomial a * X^s
C a is the constant polynomial with value a
X n is the polynomial with value X_n
The coefficient of the monomial m in the multi-variable polynomial p.
Evaluate a polynomial p given a valuation g of all the variables and a ring hom f from the scalar ring to the target
Evaluate a polynomial p given a valuation f of all the variables
map f p maps a polynomial p across a ring hom f
The maximal degrees of each variable in a multi-variable polynomial, expressed as a multiset.
(For example, degrees (x^2 * y + y^3) would be {x, x, y, y, y}.)
vars p is the set of variables appearing in the polynomial p
degree_of n p gives the highest power of X_n that appears in p
total_degree p gives the maximum |s| over the monomials X^s in p
A ring homomorphism f : Z[X_1, X_2, ...] → R is determined by the evaluations f(X_1), f(X_2), ...
Ring homomorphisms out of integer polynomials on a type σ are the same as functions out of the type σ,
Rename all the variables in a multivariable polynomial.
The ring isomorphism between multivariable polynomials in no variables and the ground ring.
The ring isomorphism between multivariable polynomials in a single variable and polynomials over the ground ring.
The ring isomorphism between multivariable polynomials induced by an equivalence of the variables.
The ring isomorphism between multivariable polynomials induced by a ring isomorphism of the ground ring.
The function from multivariable polynomials in a sum of two types, to multivariable polynomials in one of the types, with coefficents in multivariable polynomials in the other type.
See sum_ring_equiv for the ring isomorphism.
The function from multivariable polynomials in one type, with coefficents in multivariable polynomials in another type, to multivariable polynomials in the sum of the two types.
See sum_ring_equiv for the ring isomorphism.
A helper function for sum_ring_equiv.
The ring isomorphism between multivariable polynomials in a sum of two types, and multivariable polynomials in one of the types, with coefficents in multivariable polynomials in the other type.
The ring isomorphism between multivariable polynomials in option β and polynomials with coefficients in mv_polynomial β α.
The ring isomorphism between multivariable polynomials in option β and multivariable polynomials with coefficients in polynomials.