DegLex

📁 Source: Mathlib/RingTheory/MvPolynomial/MonomialOrder/DegLex.lean

Statistics

Metric	Count
Definitions DegLex	1
Theorems degLex_totalDegree_monotone, degree_degLexDegree	2
Total	3

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
degLex_totalDegree_monotone 📖	mathematical	MonomialOrder.syn MonomialOrder.degLex Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MonomialOrder.lo DFunLike.coe AddEquiv Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup MonomialOrder.acm EquivLike.toFunLike AddEquiv.instEquivLike MonomialOrder.toSyn MonomialOrder.degree	totalDegree	—	Finsupp.DegLex.monotone_degree
degree_degLexDegree 📖	mathematical	—	DFunLike.coe AddMonoidHom Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Nat.instAddCommMonoid Finsupp.instAddZeroClass AddMonoidHom.instFunLike Finsupp.degree MonomialOrder.degree MonomialOrder.degLex totalDegree	—	MonomialOrder.degree_zero map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass totalDegree_zero le_antisymm le_totalDegree MonomialOrder.degree_mem_support Finset.sup_le Finsupp.DegLex.monotone_degree MonomialOrder.le_degree

(root)

Definitions

Name	Category	Theorems
DegLex 📖	CompOp	25 math math: toDegLex_inj, toDegLex_symm_eq, toDegLex_injective, ofDegLex_symm_eq, DegLex.forall_iff, toDegLex_ofDegLex, Finsupp.DegLex.single_lt_iff, MonomialOrder.degLex_le_iff, Finsupp.DegLex.single_antitone, ofDegLex_inj, ofDegLex_toDegLex, Finsupp.DegLex.lt_iff, ofDegLex_injective, Finsupp.DegLex.single_le_iff, Finsupp.DegLex.isStrictOrder, MonomialOrder.degLex_lt_iff, Finsupp.DegLex.instIsOrderedCancelAddMonoidDegLexNat, Finsupp.DegLex.wellFoundedLT, Finsupp.DegLex.le_iff, Finsupp.DegLex.monotone_degree, ofDegLex_add, Finsupp.DegLex.lt_def, Finsupp.DegLex.single_strictAnti, DegLex.exists_iff, toDegLex_add

---

← Back to Index