Documentation Verification Report

DegLex

📁 Source: Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean

Statistics

Metric	Count
Definitions `rec`, `DegLex`, `instLTDegLexNat`, `instLinearOrderDegLexNat`, `orderBot`, `degLex`, `instAddCommMonoidDegLex`, `ofDegLex`, `toDegLex`	9
Theorems `exists_iff`, `forall_iff`, `instIsOrderedCancelAddMonoidDegLexNat`, `isStrictOrder`, `le_iff`, `lt_def`, `lt_iff`, `monotone_degree`, `single_antitone`, `single_le_iff`, `single_lt_iff`, `single_strictAnti`, `wellFounded`, `wellFoundedLT`, `degLex_def`, `degLex_le_iff`, `degLex_lt_iff`, `degLex_single_le_iff`, `degLex_single_lt_iff`, `ofDegLex_add`, `ofDegLex_inj`, `ofDegLex_injective`, `ofDegLex_symm_eq`, `ofDegLex_toDegLex`, `toDegLex_add`, `toDegLex_inj`, `toDegLex_injective`, `toDegLex_ofDegLex`, `toDegLex_symm_eq`	29
Total	38

DegLex

Definitions

Name	Category	Theorems
`rec` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_iff` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DegLex` `EquivLike.toFunLike` `Equiv.instEquivLike` `toDegLex`	—	—
`forall_iff` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DegLex` `EquivLike.toFunLike` `Equiv.instEquivLike` `toDegLex`	—	—

Finsupp

Definitions

Name	Category	Theorems
`DegLex` 📖	MathDef	2 math math: `degLex_def`, `DegLex.wellFounded`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`degLex_def` 📖	mathematical	—	`DegLex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Lex` `DFunLike.coe` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `instAddZeroClass` `AddMonoidHom.instFunLike` `degree`	—	—

Finsupp.DegLex

Definitions

Name	Category	Theorems
`instLTDegLexNat` 📖	CompOp	6 math math: `single_lt_iff`, `lt_iff`, `isStrictOrder`, `MonomialOrder.degLex_lt_iff`, `wellFoundedLT`, `lt_def`
`instLinearOrderDegLexNat` 📖	CompOp	7 math math: `MonomialOrder.degLex_le_iff`, `single_antitone`, `single_le_iff`, `instIsOrderedCancelAddMonoidDegLexNat`, `le_iff`, `monotone_degree`, `single_strictAnti`
`orderBot` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsOrderedCancelAddMonoidDegLexNat` 📖	mathematical	—	`IsOrderedCancelAddMonoid` `DegLex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instAddCommMonoidDegLex` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderDegLexNat`	—	`le_iff` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Finsupp.Lex.addRightMono` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `instIsRightCancelAddLex` `Finsupp.instIsRightCancelAdd` `Finsupp.Lex.addLeftMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddLex` `Finsupp.instIsLeftCancelAdd`
`isStrictOrder` 📖	mathematical	—	`IsStrictOrder` `DegLex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instLTDegLexNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`lt_trans`
`le_iff` 📖	mathematical	—	`DegLex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderDegLexNat` `DFunLike.coe` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofDegLex` `Lex` `Finsupp.Lex.partialOrder` `Nat.instPartialOrder` `toLex`	—	`EquivLike.toEmbeddingLike`
`lt_def` 📖	mathematical	—	`DegLex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instLTDegLexNat` `Lex` `Prod.Lex.instLT` `Finsupp.instLTLex` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree` `ofDegLex`	—	—
`lt_iff` 📖	mathematical	—	`DegLex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instLTDegLexNat` `DFunLike.coe` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofDegLex` `Lex` `Finsupp.instLTLex` `toLex`	—	—
`monotone_degree` 📖	mathematical	—	`Monotone` `DegLex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderDegLexNat` `Nat.instPreorder` `DFunLike.coe` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.degree` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofDegLex`	—	`le_iff` `le_of_lt` `le_of_eq`
`single_antitone` 📖	mathematical	—	`Antitone` `DegLex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderDegLexNat` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toDegLex` `Finsupp.single`	—	`StrictAnti.antitone` `single_strictAnti`
`single_le_iff` 📖	mathematical	—	`DegLex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderDegLexNat` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toDegLex` `Finsupp.single`	—	`StrictAnti.le_iff_ge` `single_strictAnti`
`single_lt_iff` 📖	mathematical	—	`DegLex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instLTDegLexNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toDegLex` `Finsupp.single`	—	`StrictAnti.lt_iff_gt` `single_strictAnti`
`single_strictAnti` 📖	mathematical	—	`StrictAnti` `DegLex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderDegLexNat` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toDegLex` `Finsupp.single`	—	`Finsupp.degree_single`
`wellFounded` 📖	mathematical	`Function.swap`	`Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.DegLex`	—	`WellFounded.prod_lex` `Finsupp.Lex.wellFounded'` `Set.wellFoundedOn_range` `Set.WellFoundedOn.mono` `Set.wellFoundedOn_univ` `le_refl`
`wellFoundedLT` 📖	mathematical	—	`WellFoundedLT` `DegLex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instLTDegLexNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`wellFounded` `instTrichotomousLt` `wellFounded_gt` `wellFounded_lt` `instWellFoundedLTNat` `LE.le.not_gt` `zero_le` `Nat.instCanonicallyOrderedAdd`

MonomialOrder

Definitions

Name	Category	Theorems
`degLex` 📖	CompOp	5 math math: `degLex_le_iff`, `MvPolynomial.degree_degLexDegree`, `degLex_single_le_iff`, `degLex_lt_iff`, `degLex_single_lt_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`degLex_le_iff` 📖	mathematical	—	`syn` `degLex` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `DegLex` `Finsupp.DegLex.instLinearOrderDegLexNat` `Equiv` `Equiv.instEquivLike` `toDegLex`	—	—
`degLex_lt_iff` 📖	mathematical	—	`syn` `degLex` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `DegLex` `Finsupp.DegLex.instLTDegLexNat` `Equiv` `Equiv.instEquivLike` `toDegLex`	—	—
`degLex_single_le_iff` 📖	mathematical	—	`syn` `degLex` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `Finsupp.single`	—	`degLex_le_iff` `Finsupp.DegLex.single_le_iff`
`degLex_single_lt_iff` 📖	mathematical	—	`syn` `degLex` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `Finsupp.single`	—	`degLex_lt_iff` `Finsupp.DegLex.single_lt_iff`

(root)

Definitions

Name	Category	Theorems
`instAddCommMonoidDegLex` 📖	CompOp	3 math math: `Finsupp.DegLex.instIsOrderedCancelAddMonoidDegLexNat`, `ofDegLex_add`, `toDegLex_add`
`ofDegLex` 📖	CompOp	11 math math: `toDegLex_symm_eq`, `ofDegLex_symm_eq`, `toDegLex_ofDegLex`, `ofDegLex_inj`, `ofDegLex_toDegLex`, `Finsupp.DegLex.lt_iff`, `ofDegLex_injective`, `Finsupp.DegLex.le_iff`, `Finsupp.DegLex.monotone_degree`, `ofDegLex_add`, `Finsupp.DegLex.lt_def`
`toDegLex` 📖	CompOp	15 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_toDegLex`, `Finsupp.DegLex.single_le_iff`, `MonomialOrder.degLex_lt_iff`, `Finsupp.DegLex.single_strictAnti`, `DegLex.exists_iff`, `toDegLex_add`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofDegLex_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DegLex` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofDegLex` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidDegLex`	—	—
`ofDegLex_inj` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DegLex` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofDegLex`	—	—
`ofDegLex_injective` 📖	mathematical	—	`DegLex` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofDegLex`	—	—
`ofDegLex_symm_eq` 📖	mathematical	—	`Equiv.symm` `DegLex` `ofDegLex` `toDegLex`	—	—
`ofDegLex_toDegLex` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DegLex` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofDegLex` `toDegLex`	—	—
`toDegLex_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DegLex` `EquivLike.toFunLike` `Equiv.instEquivLike` `toDegLex` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidDegLex`	—	—
`toDegLex_inj` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DegLex` `EquivLike.toFunLike` `Equiv.instEquivLike` `toDegLex`	—	—
`toDegLex_injective` 📖	mathematical	—	`DegLex` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toDegLex`	—	—
`toDegLex_ofDegLex` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DegLex` `EquivLike.toFunLike` `Equiv.instEquivLike` `toDegLex` `ofDegLex`	—	—
`toDegLex_symm_eq` 📖	mathematical	—	`Equiv.symm` `DegLex` `toDegLex` `ofDegLex`	—	—

---

← Back to Index