Documentation Verification Report

Lex

📁 Source: Mathlib/Data/Finsupp/Lex.lean

Statistics

Metric	Count
Definitions `linearOrder`, `orderBot`, `partialOrder`, `Lex`, `linearOrder`, `orderBot`, `partialOrder`, `instLTColex`, `instLTLex`	9
Theorems `addLeftMono`, `addLeftStrictMono`, `addRightMono`, `addRightStrictMono`, `isOrderedCancelAddMonoid`, `isStrictOrder`, `le_iff_of_unique`, `lt_iff`, `lt_iff_of_unique`, `single_le_iff`, `single_lt_iff`, `single_strictMono`, `addLeftMono`, `addLeftStrictMono`, `addRightMono`, `addRightStrictMono`, `isOrderedCancelAddMonoid`, `isStrictOrder`, `le_iff_of_unique`, `lt_iff`, `lt_iff_of_unique`, `single_antitone`, `single_le_iff`, `single_lt_iff`, `single_strictAnti`, `lex_def`, `lex_eq_invImage_dfinsupp_lex`, `lex_iff_of_unique`, `lex_le_iff_of_unique`, `lex_lt_iff`, `lex_lt_iff_of_unique`, `lex_lt_of_lt`, `lex_lt_of_lt_of_preorder`, `lt_of_forall_lt_of_lt`, `toColex_monotone`, `toLex_monotone`, `lex_eq_finsupp_lex`	37
Total	46

Finsupp

Definitions

Name	Category	Theorems
`Lex` 📖	MathDef	10 math math: `Lex.wellFounded'`, `lex_iff_of_unique`, `Relation.cutExpand_le_invImage_lex`, `degLex_def`, `lex_eq_invImage_dfinsupp_lex`, `Lex.wellFounded`, `lex_def`, `Lex.wellFounded_of_finite`, `Lex.acc`, `Pi.lex_eq_finsupp_lex`
`instLTColex` 📖	CompOp	8 math math: `Colex.addLeftStrictMono`, `Colex.isStrictOrder`, `Colex.wellFoundedLT`, `Colex.addRightStrictMono`, `Colex.wellFoundedLT_of_finite`, `Colex.lt_iff`, `Colex.single_lt_iff`, `Colex.lt_iff_of_unique`
`instLTLex` 📖	CompOp	15 math math: `MvPowerSeries.lexOrder_def_of_ne_zero`, `Lex.isStrictOrder`, `lt_of_forall_lt_of_lt`, `Lex.single_lt_iff`, `DegLex.lt_iff`, `lex_lt_iff_of_unique`, `Lex.addRightStrictMono`, `Lex.addLeftStrictMono`, `lex_lt_iff`, `MonomialOrder.lex_lt_iff`, `Lex.wellFoundedLT`, `Lex.lt_iff`, `DegLex.lt_def`, `Lex.wellFoundedLT_of_finite`, `Lex.lt_iff_of_unique`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lex_def` 📖	mathematical	—	`Lex` `DFunLike.coe` `Finsupp` `instFunLike`	—	—
`lex_eq_invImage_dfinsupp_lex` 📖	mathematical	—	`Lex` `Finsupp` `DFinsupp` `DFinsupp.Lex` `toDFinsupp`	—	—
`lex_iff_of_unique` 📖	mathematical	—	`Lex` `DFunLike.coe` `Finsupp` `instFunLike` `Unique.instInhabited`	—	`Pi.lex_iff_of_unique`
`lex_le_iff_of_unique` 📖	mathematical	—	`Lex` `Finsupp` `Preorder.toLE` `PartialOrder.toPreorder` `Lex.partialOrder` `DFunLike.coe` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `Unique.instInhabited`	—	`Lex.le_iff_of_unique`
`lex_lt_iff` 📖	mathematical	—	`Lex` `Finsupp` `instLTLex` `DFunLike.coe` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	`Lex.lt_iff`
`lex_lt_iff_of_unique` 📖	mathematical	—	`Lex` `Finsupp` `instLTLex` `Preorder.toLT` `DFunLike.coe` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `Unique.instInhabited`	—	`Lex.lt_iff_of_unique`
`lex_lt_of_lt` 📖	mathematical	`Finsupp` `Preorder.toLT` `preorder` `PartialOrder.toPreorder`	`Pi.Lex` `DFunLike.coe` `instFunLike`	—	`DFinsupp.lex_lt_of_lt`
`lex_lt_of_lt_of_preorder` 📖	mathematical	`Finsupp` `Preorder.toLT` `preorder`	`Preorder.toLE` `DFunLike.coe` `instFunLike`	—	`DFinsupp.lex_lt_of_lt_of_preorder`
`lt_of_forall_lt_of_lt` 📖	mathematical	`DFunLike.coe` `Finsupp` `instFunLike` `Equiv` `Lex` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `Preorder.toLT` `PartialOrder.toPreorder`	`instLTLex` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—
`toColex_monotone` 📖	mathematical	—	`Monotone` `Finsupp` `Colex` `preorder` `PartialOrder.toPreorder` `Colex.partialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex`	—	`toLex_monotone`
`toLex_monotone` 📖	mathematical	—	`Monotone` `Finsupp` `Lex` `preorder` `PartialOrder.toPreorder` `Lex.partialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`DFinsupp.toLex_monotone`

Finsupp.Colex

Definitions

Name	Category	Theorems
`linearOrder` 📖	CompOp	—
`orderBot` 📖	CompOp	—
`partialOrder` 📖	CompOp	7 math math: `Finsupp.toColex_monotone`, `isOrderedCancelAddMonoid`, `addRightMono`, `le_iff_of_unique`, `addLeftMono`, `single_le_iff`, `single_strictMono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLeftMono` 📖	mathematical	—	`AddLeftMono` `Colex` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddColex` `Finsupp.instAdd` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`addLeftMono_of_addLeftStrictMono` `addLeftStrictMono`
`addLeftStrictMono` 📖	mathematical	—	`AddLeftStrictMono` `Colex` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddColex` `Finsupp.instAdd` `Finsupp.instLTColex` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Finsupp.Lex.addLeftStrictMono`
`addRightMono` 📖	mathematical	—	`AddRightMono` `Colex` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddColex` `Finsupp.instAdd` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`addRightMono_of_addRightStrictMono` `addRightStrictMono`
`addRightStrictMono` 📖	mathematical	—	`AddRightStrictMono` `Colex` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddColex` `Finsupp.instAdd` `Finsupp.instLTColex` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Finsupp.Lex.addRightStrictMono`
`isOrderedCancelAddMonoid` 📖	mathematical	—	`IsOrderedCancelAddMonoid` `Colex` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidColex` `Finsupp.instAddCommMonoid` `partialOrder`	—	`Finsupp.Lex.isOrderedCancelAddMonoid`
`isStrictOrder` 📖	mathematical	—	`IsStrictOrder` `Colex` `Finsupp` `Finsupp.instLTColex` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Finsupp.Lex.isStrictOrder`
`le_iff_of_unique` 📖	mathematical	—	`Colex` `Finsupp` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `DFunLike.coe` `Finsupp.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofColex` `Unique.instInhabited`	—	`Finsupp.Lex.le_iff_of_unique`
`lt_iff` 📖	mathematical	—	`Colex` `Finsupp` `Finsupp.instLTColex` `DFunLike.coe` `Finsupp.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofColex`	—	—
`lt_iff_of_unique` 📖	mathematical	—	`Colex` `Finsupp` `Finsupp.instLTColex` `Preorder.toLT` `DFunLike.coe` `Finsupp.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofColex` `Unique.instInhabited`	—	`Finsupp.Lex.lt_iff_of_unique`
`single_le_iff` 📖	mathematical	—	`Colex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `Nat.instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finsupp.single` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`StrictMono.le_iff_le` `single_strictMono`
`single_lt_iff` 📖	mathematical	—	`Colex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instLTColex` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finsupp.single`	—	`StrictMono.lt_iff_lt` `single_strictMono`
`single_strictMono` 📖	mathematical	—	`StrictMono` `Colex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `partialOrder` `Nat.instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Finsupp.single`	—	`Finsupp.Lex.single_strictAnti`

Finsupp.Lex

Definitions

Name	Category	Theorems
`linearOrder` 📖	CompOp	9 math math: `MvPowerSeries.min_lexOrder_le`, `MvPolynomial.supDegree_esymmAlgHomMonomial`, `MvPolynomial.leadingCoeff_esymmAlgHomMonomial`, `MvPolynomial.supDegree_esymm`, `MvPolynomial.leadingCoeff_toLex_C`, `MvPolynomial.monic_esymm`, `MvPolynomial.supDegree_toLex_C`, `MvPolynomial.IsSymmetric.antitone_supDegree`, `MvPolynomial.leadingCoeff_toLex`
`orderBot` 📖	CompOp	8 math math: `MvPolynomial.supDegree_esymmAlgHomMonomial`, `MvPolynomial.leadingCoeff_esymmAlgHomMonomial`, `MvPolynomial.supDegree_esymm`, `MvPolynomial.leadingCoeff_toLex_C`, `MvPolynomial.monic_esymm`, `MvPolynomial.supDegree_toLex_C`, `MvPolynomial.IsSymmetric.antitone_supDegree`, `MvPolynomial.leadingCoeff_toLex`
`partialOrder` 📖	CompOp	17 math math: `instIsOrderedCancelAddMonoidLexFinsupp`, `MvPowerSeries.min_lexOrder_le`, `addLeftMono`, `single_strictAnti`, `MvPowerSeries.le_lexOrder_iff`, `le_iff_of_unique`, `single_antitone`, `Finsupp.lex_le_iff_of_unique`, `isOrderedCancelAddMonoid`, `Finsupp.DegLex.le_iff`, `MonomialOrder.lex_le_iff`, `addRightMono`, `MvPowerSeries.lexOrder_le_of_coeff_ne_zero`, `Finsupp.toLex_monotone`, `single_le_iff`, `MvPowerSeries.le_lexOrder_mul`, `MvPowerSeries.lexOrder_mul_ge`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLeftMono` 📖	mathematical	—	`AddLeftMono` `Lex` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddLex` `Finsupp.instAdd` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`addLeftMono_of_addLeftStrictMono` `addLeftStrictMono`
`addLeftStrictMono` 📖	mathematical	—	`AddLeftStrictMono` `Lex` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddLex` `Finsupp.instAdd` `Finsupp.instLTLex` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`add_lt_add_right`
`addRightMono` 📖	mathematical	—	`AddRightMono` `Lex` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddLex` `Finsupp.instAdd` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`addRightMono_of_addRightStrictMono` `addRightStrictMono`
`addRightStrictMono` 📖	mathematical	—	`AddRightStrictMono` `Lex` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddLex` `Finsupp.instAdd` `Finsupp.instLTLex` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`add_lt_add_left`
`isOrderedCancelAddMonoid` 📖	mathematical	—	`IsOrderedCancelAddMonoid` `Lex` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidLex` `Finsupp.instAddCommMonoid` `partialOrder`	—	`add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `Pi.Lex.isOrderedAddCancelMonoid` `le_of_add_le_add_left` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddLex` `Pi.instIsLeftCancelAdd` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsOrderedCancelAddMonoid.toAddLeftReflectLT`
`isStrictOrder` 📖	mathematical	—	`IsStrictOrder` `Lex` `Finsupp` `Finsupp.instLTLex` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`lt_irrefl` `lt_trans`
`le_iff_of_unique` 📖	mathematical	—	`Lex` `Finsupp` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `DFunLike.coe` `Finsupp.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `Unique.instInhabited`	—	`Pi.lex_le_iff_of_unique`
`lt_iff` 📖	mathematical	—	`Lex` `Finsupp` `Finsupp.instLTLex` `DFunLike.coe` `Finsupp.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	—
`lt_iff_of_unique` 📖	mathematical	—	`Lex` `Finsupp` `Finsupp.instLTLex` `Preorder.toLT` `DFunLike.coe` `Finsupp.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `Unique.instInhabited`	—	`Finsupp.lex_iff_of_unique` `instIrreflLt`
`single_antitone` 📖	mathematical	—	`Antitone` `Lex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `partialOrder` `Nat.instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `Finsupp.single`	—	`StrictAnti.antitone` `single_strictAnti`
`single_le_iff` 📖	mathematical	—	`Lex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `Nat.instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `Finsupp.single` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`StrictAnti.le_iff_ge` `single_strictAnti`
`single_lt_iff` 📖	mathematical	—	`Lex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instLTLex` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `Finsupp.single`	—	`StrictAnti.lt_iff_gt` `single_strictAnti`
`single_strictAnti` 📖	mathematical	—	`StrictAnti` `Lex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `partialOrder` `Nat.instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `Finsupp.single`	—	`Finsupp.single_eq_of_ne` `LT.lt.ne` `LT.lt.trans` `Finsupp.single_eq_of_ne'` `LT.lt.ne'` `Finsupp.single_eq_same` `Nat.instZeroLEOneClass`

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lex_eq_finsupp_lex` 📖	mathematical	—	`Lex` `DFunLike.coe` `Finsupp` `Finsupp.instFunLike` `Finsupp.Lex`	—	—

---

← Back to Index