Degrees of polynomials #
This file establishes many results about the degree of a multivariate polynomial.
The degree set of a polynomial $P \in R[X]$ is a Multiset
containing, for each $x$ in the
variable set, $n$ copies of $x$, where $n$ is the maximum number of copies of $x$ appearing in a
monomial of $P$.
Main declarations #
-
MvPolynomial.degrees p
: the multiset of variables representing the union of the multisets corresponding to each non-zero monomial inp
. For example if7 ≠ 0
inR
andp = x²y+7y³
thendegrees p = {x, x, y, y, y}
-
MvPolynomial.degreeOf n p : ℕ
: the total degree ofp
with respect to the variablen
. For example ifp = x⁴y+yz
thendegreeOf y p = 1
. -
MvPolynomial.totalDegree p : ℕ
: the max of the sizes of the multisetss
whose monomialsX^s
occur inp
. For example ifp = x⁴y+yz
thentotalDegree p = 5
.
Notation #
As in other polynomial files, we typically use the notation:
-
σ τ : Type*
(indexing the variables) -
R : Type*
[CommSemiring R]
(the coefficients) -
s : σ →₀ ℕ
, a function fromσ
toℕ
which is zero away from a finite set. This will give rise to a monomial inMvPolynomial σ R
which mathematicians might callX^s
-
r : R
-
i : σ
, with corresponding monomialX i
, often denotedX_i
by mathematicians -
p : MvPolynomial σ R
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}
.)
Equations
- MvPolynomial.degrees p = Finset.sup (MvPolynomial.support p) fun (s : σ →₀ ℕ) => Finsupp.toMultiset s
Instances For
degreeOf n p
gives the highest power of X_n that appears in p
Equations
Instances For
totalDegree p
gives the maximum |s| over the monomials X^s in p
Equations
- MvPolynomial.totalDegree p = Finset.sup (MvPolynomial.support p) fun (s : σ →₀ ℕ) => Finsupp.sum s fun (x : σ) (e : ℕ) => e