Documentation
Mathlib
.
RingTheory
.
MvPolynomial
.
MonomialOrder
.
DegLex
Search
return to top
source
Imports
Init
Mathlib.RingTheory.MvPolynomial.MonomialOrder
Mathlib.Data.Finsupp.MonomialOrder.DegLex
Imported by
MvPolynomial
.
degree_degLexDegree
MvPolynomial
.
degLex_totalDegree_monotone
Some lemmas about the deglex monomial order on multivariate polynomials
#
source
theorem
MvPolynomial
.
degree_degLexDegree
{σ :
Type
u_1}
[
LinearOrder
σ
]
{R :
Type
u_2}
[
CommSemiring
R
]
[
WellFoundedGT
σ
]
{f :
MvPolynomial
σ
R
}
:
(
MonomialOrder.degLex
.
degree
f
)
.
degree
=
f
.
totalDegree
source
theorem
MvPolynomial
.
degLex_totalDegree_monotone
{σ :
Type
u_1}
[
LinearOrder
σ
]
{R :
Type
u_2}
[
CommSemiring
R
]
[
WellFoundedGT
σ
]
{f g :
MvPolynomial
σ
R
}
(h :
MonomialOrder.degLex
.
toSyn
(
MonomialOrder.degLex
.
degree
f
)
≤
MonomialOrder.degLex
.
toSyn
(
MonomialOrder.degLex
.
degree
g
)
)
:
f
.
totalDegree
≤
g
.
totalDegree