Documentation Verification Report

LexOrder

📁 Source: Mathlib/RingTheory/MvPowerSeries/LexOrder.lean

Statistics

Metric	Count
Definitions `lexOrder`	1
Theorems `coeff_eq_zero_of_lt_lexOrder`, `coeff_mul_of_add_lexOrder`, `coeff_ne_zero_of_lexOrder`, `exists_finsupp_eq_lexOrder_of_ne_zero`, `le_lexOrder_iff`, `le_lexOrder_mul`, `lexOrder_def_of_ne_zero`, `lexOrder_eq_top_iff_eq_zero`, `lexOrder_le_of_coeff_ne_zero`, `lexOrder_mul`, `lexOrder_mul_ge`, `lexOrder_zero`, `min_lexOrder_le`	13
Total	14

MvPowerSeries

Definitions

Name	Category	Theorems
`lexOrder` 📖	CompOp	10 math math: `exists_finsupp_eq_lexOrder_of_ne_zero`, `min_lexOrder_le`, `lexOrder_def_of_ne_zero`, `lexOrder_mul`, `le_lexOrder_iff`, `lexOrder_zero`, `lexOrder_eq_top_iff_eq_zero`, `lexOrder_le_of_coeff_ne_zero`, `le_lexOrder_mul`, `lexOrder_mul_ge`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_eq_zero_of_lt_lexOrder` 📖	mathematical	`WithTop` `Lex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `Finsupp.Lex.partialOrder` `Nat.instPartialOrder` `WithTop.some` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `lexOrder`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `wellFounded_lt` `Finsupp.Lex.wellFoundedLT` `instTrichotomousLt` `Nat.instCanonicallyOrderedAdd` `instWellFoundedLTNat` `lexOrder_def_of_ne_zero` `WellFounded.not_lt_min` `Set.mem_image_equiv` `WithTop.coe_lt_coe`
`coeff_mul_of_add_lexOrder` 📖	mathematical	`lexOrder` `WithTop.some` `Lex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`coeff_mul` `Finset.sum_eq_single_of_mem` `trichotomy_of_add_eq_add` `Finsupp.Lex.addLeftStrictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finsupp.Lex.addRightStrictMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `contravariant_lt_of_covariant_le` `covariant_swap_add_of_covariant_add` `coeff_eq_zero_of_lt_lexOrder` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero`
`coeff_ne_zero_of_lexOrder` 📖	—	`WithTop.some` `Lex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `lexOrder`	—	—	`wellFounded_lt` `Finsupp.Lex.wellFoundedLT` `instTrichotomousLt` `Nat.instCanonicallyOrderedAdd` `instWellFoundedLTNat` `lexOrder_def_of_ne_zero` `WellFounded.min_mem`
`exists_finsupp_eq_lexOrder_of_ne_zero` 📖	mathematical	—	`Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `lexOrder` `WithTop.some` `Lex` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`le_lexOrder_iff` 📖	mathematical	—	`WithTop` `Lex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `Finsupp.Lex.partialOrder` `Nat.instPartialOrder` `lexOrder` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`coeff_eq_zero_of_lt_lexOrder` `lt_of_lt_of_le` `not_lt` `lexOrder_eq_top_iff_eq_zero` `ne_top_of_lt` `exists_finsupp_eq_lexOrder_of_ne_zero` `coeff_ne_zero_of_lexOrder`
`le_lexOrder_mul` 📖	mathematical	—	`WithTop` `Lex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `Finsupp.Lex.partialOrder` `Nat.instPartialOrder` `WithTop.add` `instAddLex` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `lexOrder` `MvPowerSeries` `instMul`	—	`le_lexOrder_iff` `coeff_mul` `Finset.sum_eq_zero` `not_lt` `not_le` `add_le_add` `WithTop.addLeftMono` `Finsupp.Lex.addLeftMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithTop.addRightMono` `Finsupp.Lex.addRightMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `contravariant_lt_of_covariant_le` `covariant_swap_add_of_covariant_add` `coeff_eq_zero_of_lt_lexOrder` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero`
`lexOrder_def_of_ne_zero` 📖	mathematical	—	`Set.Nonempty` `Lex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Set.image` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `Function.support` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `lexOrder` `WithTop.some` `WellFounded.min` `Finsupp.instLTLex` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `wellFounded_lt` `Finsupp.Lex.wellFoundedLT` `instTrichotomousLt` `Nat.instAddMonoid` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `instWellFoundedLTNat`	—	`wellFounded_lt` `Finsupp.Lex.wellFoundedLT` `instTrichotomousLt` `Nat.instCanonicallyOrderedAdd` `instWellFoundedLTNat`
`lexOrder_eq_top_iff_eq_zero` 📖	mathematical	—	`lexOrder` `Top.top` `WithTop` `Lex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `WithTop.top` `MvPowerSeries` `instZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`lexOrder_le_of_coeff_ne_zero` 📖	mathematical	—	`WithTop` `Lex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `Finsupp.Lex.partialOrder` `Nat.instPartialOrder` `lexOrder` `WithTop.some` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`not_lt` `coeff_eq_zero_of_lt_lexOrder`
`lexOrder_mul` 📖	mathematical	—	`lexOrder` `MvPowerSeries` `instMul` `WithTop` `Lex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `WithTop.add` `instAddLex` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	`eq_or_ne` `lexOrder.congr_simp` `MulZeroClass.zero_mul` `lexOrder_zero` `MulZeroClass.mul_zero` `WithTop.add_top` `exists_finsupp_eq_lexOrder_of_ne_zero` `le_antisymm` `lexOrder_le_of_coeff_ne_zero` `coeff_mul_of_add_lexOrder` `mul_ne_zero_iff` `coeff_ne_zero_of_lexOrder` `lexOrder_mul_ge`
`lexOrder_mul_ge` 📖	mathematical	—	`WithTop` `Lex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `Finsupp.Lex.partialOrder` `Nat.instPartialOrder` `WithTop.add` `instAddLex` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `lexOrder` `MvPowerSeries` `instMul`	—	`le_lexOrder_mul`
`lexOrder_zero` 📖	mathematical	—	`lexOrder` `MvPowerSeries` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Top.top` `WithTop` `Lex` `Finsupp` `Nat.instMulZeroClass` `WithTop.top`	—	—
`min_lexOrder_le` 📖	mathematical	—	`WithTop` `Lex` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `Finsupp.Lex.partialOrder` `Nat.instPartialOrder` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Finsupp.Lex.linearOrder` `Nat.instLinearOrder` `lexOrder` `MvPowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring`	—	`le_lexOrder_iff` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `coeff_eq_zero_of_lt_lexOrder` `add_zero`

---

← Back to Index