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 σ R which mathematicians might call
a : R
i : σ, with corresponding monomial
X i, often denoted
X_i by mathematicians
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