Degree and leading coefficient of polynomials with respect to a monomial order #
We consider a type σ
of indeterminates and a commutative semiring R
and a monomial order m : MonomialOrder σ
.
m.degree f
is the degree off
for the monomial orderingm
m.leadingCoeff f
is the leading coefficient off
for the monomial orderingm
m.leadingCoeff_ne_zero_iff f
asserts that this coefficient is nonzero ifff ≠ 0
.in a field,
m.isUnit_leadingCoeff f
asserts that this coefficient is a unit ifff ≠ 0
.m.degree_add_le
: them.degree
off + g
is smaller than or equal to the supremum of those off
andg
m.degree_add_of_lt h
: them.degree
off + g
is equal to that off
if them.degree
ofg
is strictly smaller than thatf
m.leadingCoeff_add_of_lt h
: then, the leading coefficient off + g
is that off
.m.degree_add_of_ne h
: them.degree
off + g
is equal to that the supremum of those off
andg
if they are distinctm.degree_sub_le
: them.degree
off - g
is smaller than or equal to the supremum of those off
andg
m.degree_sub_of_lt h
: them.degree
off - g
is equal to that off
if them.degree
ofg
is strictly smaller than thatf
m.leadingCoeff_sub_of_lt h
: then, the leading coefficient off - g
is that off
.m.degree_mul_le
: them.degree
off * g
is smaller than or equal to the sum of those off
andg
.m.degree_mul_of_isRegular_left
,m.degree_mul_of_isRegular_right
andm.degree_mul
assert the equality when the leading coefficient off
org
is regular, or whenR
is a domain andf
andg
are nonzero.m.leadingCoeff_mul_of_isRegular_left
,m.leadingCoeff_mul_of_isRegular_right
andm.leadingCoeff_mul
say thatm.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Reference #
the degree of a multivariate polynomial with respect to a monomial ordering
Instances For
the leading coefficient of a multivariate polynomial with respect to a monomial ordering
Equations
- m.leadingCoeff f = MvPolynomial.coeff (m.degree f) f
Instances For
Alias of MonomialOrder.leadingCoeff
.
the leading coefficient of a multivariate polynomial with respect to a monomial ordering
Equations
Instances For
Alias of MonomialOrder.leadingCoeff_zero
.
Alias of MonomialOrder.leadingCoeff_monomial
.
Alias of MonomialOrder.leadingCoeff_ne_zero_iff
.
Alias of MonomialOrder.leadingCoeff_eq_zero_iff
.
Alias of MonomialOrder.leadingCoeff_add_of_lt
.
Multiplicativity of leading coefficients
Multiplicativity of leading coefficients
Multiplicativity of leading coefficients
Multiplicativity of leading coefficients
Alias of MonomialOrder.leadingCoeff_mul_of_isRegular_left
.
Multiplicativity of leading coefficients
Multiplicativity of leading coefficients
Multiplicativity of leading coefficients
Alias of MonomialOrder.leadingCoeff_mul_of_isRegular_right
.
Multiplicativity of leading coefficients
Degree of product
Degree of of product
Multiplicativity of leading coefficients
Alias of MonomialOrder.leadingCoeff_mul
.
Multiplicativity of leading coefficients
Alias of MonomialOrder.leadingCoeff_sub_of_lt
.
Alias of MonomialOrder.isUnit_leadingCoeff
.