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*
[CommRing R](the coefficients)
s : σ →₀ ℕ, a function from
ℕwhich is zero away from a finite set. This will give rise to a monomial in
MvPolynomial σ Rwhich mathematicians might call
a : R
i : σ, with corresponding monomial
X i, often denoted
p : MvPolynomial σ R