Multivariate polynomials over a ring #
Many results about polynomials hold when the coefficient ring is a commutative semiring. Some stronger results can be derived when we assume this semiring is a ring.
This file does not define any new operations, but proves some of these stronger results.
As in other polynomial files, we typically use the notation:
σ : Type*(indexing the variables)
R : Type*
[comm_ring R](the coefficients)
s : σ →₀ ℕ, a function from
ℕwhich is zero away from a finite set. This will give rise to a monomial in
mv_polynomial σ Rwhich mathematicians might call
a : R
i : σ, with corresponding monomial
X i, often denoted
p : mv_polynomial σ R
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