Degrees of polynomials #
This file establishes many results about the degree of a multivariate polynomial.
The degree set of a polynomial Multiset
containing, for each
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 mathematiciansp : 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}
.)
Instances For
Alias of MvPolynomial.degrees_add_le
.
Alias of MvPolynomial.degrees_sum_le
.
Alias of MvPolynomial.degrees_mul_le
.
Alias of MvPolynomial.degrees_prod_le
.
Alias of MvPolynomial.degrees_pow_le
.
Alias of MvPolynomial.le_degrees_add_left
.
Alias of MvPolynomial.degrees_map_le
.
degreeOf n p
gives the highest power of X_n that appears in p
Equations
- MvPolynomial.degreeOf n p = Multiset.count n p.degrees
Instances For
Alias of MvPolynomial.degreeOf_mul_X_of_ne
.
Alias of MvPolynomial.degreeOf_mul_X_self
.
totalDegree p
gives the maximum |s| over the monomials X^s in p
Instances For
The submodule of multivariate polynomials of degrees bounded by a monomial s
.
Equations
- MvPolynomial.degreesLE R σ s = { carrier := {p : MvPolynomial σ R | p.degrees ≤ s}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }