Lex

📁 Source: Mathlib/RingTheory/HahnSeries/Lex.lean

Statistics

Metric	Count
Definitions archimedeanClassOrderIsoWithTop, embDomainOrderAddMonoidHom, embDomainOrderEmbedding, finiteArchimedeanClassOrderHomInvLex, finiteArchimedeanClassOrderHomLex, finiteArchimedeanClassOrderIso, finiteArchimedeanClassOrderIsoLex, instLinearOrderLex, instPartialOrderLex, Lex, Lex	11
Theorems abs_lt_abs_of_orderTop_ofLex, archimedeanClassMk_eq_archimedeanClassMk_iff, archimedeanClassMk_le_archimedeanClassMk_iff, archimedeanClassMk_le_archimedeanClassMk_iff_of_orderTop_ofLex, archimedeanClassOrderIsoWithTop_apply, embDomainOrderAddMonoidHom_apply, embDomainOrderAddMonoidHom_injective, embDomainOrderEmbedding_apply, finiteArchimedeanClassOrderIsoLex_apply_fst, finiteArchimedeanClassOrderIsoLex_apply_snd, finiteArchimedeanClassOrderIso_apply, instIsOrderedAddMonoidLex, instIsOrderedRingLexOfNoZeroDivisors, instIsStrictOrderedRingLexOfIsDomain, leadingCoeff_abs, leadingCoeff_neg_iff, leadingCoeff_nonneg_iff, leadingCoeff_nonpos_iff, leadingCoeff_pos_iff, lt_iff, orderTop_abs, order_abs, support_abs	23
Total	34

HahnSeries

Definitions

Name	Category	Theorems
archimedeanClassOrderIsoWithTop 📖	CompOp	1 math math: archimedeanClassOrderIsoWithTop_apply
embDomainOrderAddMonoidHom 📖	CompOp	2 math math: embDomainOrderAddMonoidHom_injective, embDomainOrderAddMonoidHom_apply
embDomainOrderEmbedding 📖	CompOp	2 math math: embDomainOrderEmbedding_apply, embDomainOrderAddMonoidHom_apply
finiteArchimedeanClassOrderHomInvLex 📖	CompOp	—
finiteArchimedeanClassOrderHomLex 📖	CompOp	—
finiteArchimedeanClassOrderIso 📖	CompOp	1 math math: finiteArchimedeanClassOrderIso_apply
finiteArchimedeanClassOrderIsoLex 📖	CompOp	2 math math: finiteArchimedeanClassOrderIsoLex_apply_snd, finiteArchimedeanClassOrderIsoLex_apply_fst
instLinearOrderLex 📖	CompOp	13 math math: HahnEmbedding.Partial.archimedeanClassMk_eq_iff, support_abs, abs_lt_abs_of_orderTop_ofLex, order_abs, archimedeanClassMk_eq_archimedeanClassMk_iff, finiteArchimedeanClassOrderIsoLex_apply_snd, archimedeanClassOrderIsoWithTop_apply, archimedeanClassMk_le_archimedeanClassMk_iff_of_orderTop_ofLex, archimedeanClassMk_le_archimedeanClassMk_iff, finiteArchimedeanClassOrderIsoLex_apply_fst, orderTop_abs, finiteArchimedeanClassOrderIso_apply, leadingCoeff_abs
instPartialOrderLex 📖	CompOp	23 math math: HahnEmbedding.Seed.baseEmbedding_pos, instIsStrictOrderedRingLexOfIsDomain, HahnEmbedding.Seed.baseEmbedding_strictMono, abs_lt_abs_of_orderTop_ofLex, HahnEmbedding.Partial.toOrderAddMonoidHom_apply, HahnEmbedding.Partial.extendFun_strictMono, HahnEmbedding.IsPartial.strictMono, embDomainOrderEmbedding_apply, leadingCoeff_pos_iff, embDomainOrderAddMonoidHom_injective, leadingCoeff_nonneg_iff, hahnEmbedding_isOrderedModule_rat, embDomainOrderAddMonoidHom_apply, HahnEmbedding.Partial.eval_lt, lt_iff, instIsOrderedAddMonoidLex, instIsOrderedRingLexOfNoZeroDivisors, HahnEmbedding.Partial.sSupFun_strictMono, leadingCoeff_neg_iff, leadingCoeff_nonpos_iff, hahnEmbedding_isOrderedAddMonoid, hahnEmbedding_isOrderedModule, HahnEmbedding.Partial.toOrderAddMonoidHom_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_lt_abs_of_orderTop_ofLex 📖	mathematical	WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder orderTop NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DFunLike.coe Equiv Lex HahnSeries EquivLike.toFunLike Equiv.instEquivLike ofLex	instPartialOrderLex abs instLinearOrderLex instAddGroupLex instAddGroup AddCommGroup.toAddGroup	—	lt_iff LT.lt.ne_top orderTop_abs coeff_eq_zero_of_lt_orderTop LT.lt.trans' WithTop.coe_untop coeff_untop_eq_leadingCoeff IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidLex IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd covariant_swap_add_of_covariant_add
archimedeanClassMk_eq_archimedeanClassMk_iff 📖	mathematical	—	Lex HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupLex instAddCommGroup instLinearOrderLex instIsOrderedAddMonoidLex AddCommGroup.toAddCommMonoid IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddLeftCancelSemigroup.toIsLeftCancelAdd AddLeftCancelMonoid.toAddLeftCancelSemigroup AddCancelCommMonoid.toAddLeftCancelMonoid AddCommGroup.toAddCancelCommMonoid IsOrderedAddMonoid.toAddLeftMono orderTop DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofLex leadingCoeff	—	instIsOrderedAddMonoidLex IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono le_antisymm_iff archimedeanClassMk_le_archimedeanClassMk_iff instIsEmptyFalse le_antisymm Eq.le Eq.ge
archimedeanClassMk_le_archimedeanClassMk_iff 📖	mathematical	—	ArchimedeanClass Lex HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupLex instAddCommGroup instLinearOrderLex instIsOrderedAddMonoidLex AddCommGroup.toAddCommMonoid IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddLeftCancelSemigroup.toIsLeftCancelAdd AddLeftCancelMonoid.toAddLeftCancelSemigroup AddCancelCommMonoid.toAddLeftCancelMonoid AddCommGroup.toAddCancelCommMonoid IsOrderedAddMonoid.toAddLeftMono Preorder.toLE PartialOrder.toPreorder ArchimedeanClass.instLinearOrder WithTop Preorder.toLT WithTop.instPreorder orderTop DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofLex leadingCoeff	—	instIsOrderedAddMonoidLex IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono lt_trichotomy one_smul LT.lt.le abs_lt_abs_of_orderTop_ofLex archimedeanClassMk_le_archimedeanClassMk_iff_of_orderTop_ofLex Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq abs_nsmul lt_of_lt_of_le orderTop_smul_not_lt LT.lt.not_gt LT.lt.ne' instIsEmptyFalse
archimedeanClassMk_le_archimedeanClassMk_iff_of_orderTop_ofLex 📖	mathematical	orderTop SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DFunLike.coe Equiv Lex HahnSeries EquivLike.toFunLike Equiv.instEquivLike ofLex	ArchimedeanClass instAddCommGroupLex instAddCommGroup instLinearOrderLex instIsOrderedAddMonoidLex AddCommGroup.toAddCommMonoid IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddLeftCancelSemigroup.toIsLeftCancelAdd AddLeftCancelMonoid.toAddLeftCancelSemigroup AddCancelCommMonoid.toAddLeftCancelMonoid AddCommGroup.toAddCancelCommMonoid IsOrderedAddMonoid.toAddLeftMono Preorder.toLE PartialOrder.toPreorder ArchimedeanClass.instLinearOrder leadingCoeff	—	instIsOrderedAddMonoidLex IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono eq_or_ne abs_zero orderTop_zero nsmul_zero leadingCoeff_zero orderTop_ne_top orderTop_abs lt_of_le_of_lt nsmul_lt_nsmul_left instIsLeftCancelAddLex Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Nat.instZeroLEOneClass lt_iff covariant_swap_add_of_covariant_add leadingCoeff_of_ne_zero WithTop.untop.congr_simp lt_trichotomy coeff_eq_zero_of_lt_orderTop WithTop.untop_eq_iff LT.lt.le Eq.le WithTop.untop_lt_iff ofLex_smul coeff_smul abs_pos leadingCoeff_ne_zero
archimedeanClassOrderIsoWithTop_apply 📖	mathematical	—	DFunLike.coe OrderIso ArchimedeanClass Lex HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupLex instAddCommGroup instLinearOrderLex instIsOrderedAddMonoidLex AddCommGroup.toAddCommMonoid IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddLeftCancelSemigroup.toIsLeftCancelAdd AddLeftCancelMonoid.toAddLeftCancelSemigroup AddCancelCommMonoid.toAddLeftCancelMonoid AddCommGroup.toAddCancelCommMonoid IsOrderedAddMonoid.toAddLeftMono WithTop Preorder.toLE PartialOrder.toPreorder ArchimedeanClass.instLinearOrder WithTop.instPreorder instFunLikeOrderIso archimedeanClassOrderIsoWithTop orderTop Equiv EquivLike.toFunLike Equiv.instEquivLike ofLex	—	instIsOrderedAddMonoidLex IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono eq_or_ne TopHomClass.map_top InfTopHomClass.toTopHomClass OrderIsoClass.toInfTopHomClass OrderIso.instOrderIsoClass orderTop_zero FiniteArchimedeanClass.withTopOrderIso_symm_apply finiteArchimedeanClassOrderIso_apply
embDomainOrderAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe OrderAddMonoidHom Lex HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass PartialOrder.toPreorder instPartialOrderLex instAddZeroClassLex instAddMonoid OrderAddMonoidHom.instFunLike embDomainOrderAddMonoidHom OrderHom.toFun OrderEmbedding.toOrderHom embDomainOrderEmbedding	—	—
embDomainOrderAddMonoidHom_injective 📖	mathematical	—	Lex HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DFunLike.coe OrderAddMonoidHom PartialOrder.toPreorder instPartialOrderLex instAddZeroClassLex instAddMonoid OrderAddMonoidHom.instFunLike embDomainOrderAddMonoidHom	—	RelEmbedding.injective
embDomainOrderEmbedding_apply 📖	mathematical	—	DFunLike.coe RelEmbedding Lex HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE PartialOrder.toPreorder instPartialOrderLex RelEmbedding.instFunLike embDomainOrderEmbedding Equiv EquivLike.toFunLike Equiv.instEquivLike toLex embDomain ofLex	—	—
finiteArchimedeanClassOrderIsoLex_apply_fst 📖	mathematical	—	WithTop.some FiniteArchimedeanClass DFunLike.coe Equiv Lex EquivLike.toFunLike Equiv.instEquivLike ofLex OrderIso HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupLex instAddCommGroup instLinearOrderLex instIsOrderedAddMonoidLex AddCommGroup.toAddCommMonoid IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddLeftCancelSemigroup.toIsLeftCancelAdd AddLeftCancelMonoid.toAddLeftCancelSemigroup AddCancelCommMonoid.toAddLeftCancelMonoid AddCommGroup.toAddCancelCommMonoid IsOrderedAddMonoid.toAddLeftMono ArchimedeanClass Preorder.toLE PartialOrder.toPreorder ArchimedeanClass.instLinearOrder Top.top OrderTop.toTop ArchimedeanClass.instOrderTop Prod.Lex.instLE Preorder.toLT instFunLikeOrderIso finiteArchimedeanClassOrderIsoLex orderTop	—	instIsOrderedAddMonoidLex IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono WithTop.coe_untop
finiteArchimedeanClassOrderIsoLex_apply_snd 📖	mathematical	—	ArchimedeanClass Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ArchimedeanClass.instLinearOrder ArchimedeanClass.instOrderTop FiniteArchimedeanClass DFunLike.coe Equiv Lex EquivLike.toFunLike Equiv.instEquivLike ofLex OrderIso HahnSeries NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupLex instAddCommGroup instLinearOrderLex instIsOrderedAddMonoidLex AddCommGroup.toAddCommMonoid IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddLeftCancelSemigroup.toIsLeftCancelAdd AddLeftCancelMonoid.toAddLeftCancelSemigroup AddCancelCommMonoid.toAddLeftCancelMonoid AddCommGroup.toAddCancelCommMonoid IsOrderedAddMonoid.toAddLeftMono Prod.Lex.instLE Preorder.toLT instFunLikeOrderIso finiteArchimedeanClassOrderIsoLex leadingCoeff	—	instIsOrderedAddMonoidLex IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono
finiteArchimedeanClassOrderIso_apply 📖	mathematical	—	WithTop.some DFunLike.coe OrderIso FiniteArchimedeanClass Lex HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupLex instAddCommGroup instLinearOrderLex instIsOrderedAddMonoidLex AddCommGroup.toAddCommMonoid IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddLeftCancelSemigroup.toIsLeftCancelAdd AddLeftCancelMonoid.toAddLeftCancelSemigroup AddCancelCommMonoid.toAddLeftCancelMonoid AddCommGroup.toAddCancelCommMonoid IsOrderedAddMonoid.toAddLeftMono ArchimedeanClass Preorder.toLE PartialOrder.toPreorder ArchimedeanClass.instLinearOrder Top.top OrderTop.toTop ArchimedeanClass.instOrderTop instFunLikeOrderIso finiteArchimedeanClassOrderIso orderTop Equiv EquivLike.toFunLike Equiv.instEquivLike ofLex	—	instIsOrderedAddMonoidLex IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono finiteArchimedeanClassOrderIsoLex_apply_fst
instIsOrderedAddMonoidLex 📖	mathematical	—	IsOrderedAddMonoid Lex HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidLex instAddCommMonoid instPartialOrderLex	—	LE.le.eq_or_lt le_of_lt lt_iff add_left_strictMono covariant_swap_add_of_covariant_add
instIsOrderedRingLexOfNoZeroDivisors 📖	mathematical	—	IsOrderedRing Lex HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instSemiringLex instSemiring Ring.toSemiring instPartialOrderLex	—	instIsOrderedAddMonoidLex IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid leadingCoeff_one IsOrderedRing.toZeroLEOneClass sub_nonneg covariant_swap_add_of_covariant_add mul_sub leadingCoeff_nonneg_iff ofLex_mul leadingCoeff_mul mul_nonneg IsOrderedRing.toPosMulMono sub_mul
instIsStrictOrderedRingLexOfIsDomain 📖	mathematical	—	IsStrictOrderedRing Lex HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instSemiringLex instSemiring Ring.toSemiring instPartialOrderLex	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid IsOrderedRing.toIsStrictOrderedRing instIsOrderedRingLexOfNoZeroDivisors IsStrictOrderedRing.toIsOrderedRing IsDomain.to_noZeroDivisors instIsDomainLex instIsDomainOfIsCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd instNontrivialLex instNontrivialOfNonempty Zero.instNonempty instNontrivialOfCharZero IsStrictOrderedRing.toCharZero IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toMulPosStrictMono
leadingCoeff_abs 📖	mathematical	—	leadingCoeff SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DFunLike.coe Equiv Lex HahnSeries EquivLike.toFunLike Equiv.instEquivLike ofLex abs instLinearOrderLex instAddGroupLex instAddGroup AddCommGroup.toAddGroup	—	lt_trichotomy abs_eq_neg_self instIsOrderedAddMonoidLex IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono LT.lt.le leadingCoeff_neg_iff ofLex_neg leadingCoeff_neg abs_zero leadingCoeff_zero abs_eq_self leadingCoeff_pos_iff
leadingCoeff_neg_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder leadingCoeff DFunLike.coe Equiv Lex HahnSeries EquivLike.toFunLike Equiv.instEquivLike ofLex instPartialOrderLex instZeroLex instZero	—	—
leadingCoeff_nonneg_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder leadingCoeff DFunLike.coe Equiv Lex HahnSeries EquivLike.toFunLike Equiv.instEquivLike ofLex instPartialOrderLex instZeroLex instZero	—	LE.le.eq_or_lt le_of_eq leadingCoeff_eq_zero LT.lt.le leadingCoeff_pos_iff leadingCoeff_zero
leadingCoeff_nonpos_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder leadingCoeff DFunLike.coe Equiv Lex HahnSeries EquivLike.toFunLike Equiv.instEquivLike ofLex instPartialOrderLex instZeroLex instZero	—	—
leadingCoeff_pos_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder leadingCoeff DFunLike.coe Equiv Lex HahnSeries EquivLike.toFunLike Equiv.instEquivLike ofLex instPartialOrderLex instZeroLex instZero	—	lt_iff leadingCoeff_ne_zero LT.lt.ne orderTop_ne_top coeff_eq_zero_of_lt_orderTop WithTop.lt_untop_iff coeff_untop_eq_leadingCoeff orderTop_eq_of_le Mathlib.Tactic.Contrapose.contrapose₁ WithTop.ne_top_iff_exists WithTop.untop_eq_iff leadingCoeff_of_ne_zero
lt_iff 📖	mathematical	—	Lex HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT PartialOrder.toPreorder instPartialOrderLex coeff DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofLex	—	—
orderTop_abs 📖	mathematical	—	orderTop SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DFunLike.coe Equiv Lex HahnSeries EquivLike.toFunLike Equiv.instEquivLike ofLex abs instLinearOrderLex instAddGroupLex instAddGroup AddCommGroup.toAddGroup	—	le_total abs_eq_neg_self instIsOrderedAddMonoidLex IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono ofLex_neg orderTop_neg abs_eq_self
order_abs 📖	mathematical	—	order SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DFunLike.coe Equiv Lex HahnSeries EquivLike.toFunLike Equiv.instEquivLike ofLex abs instLinearOrderLex instAddGroupLex instAddGroup AddCommGroup.toAddGroup	—	eq_or_ne abs_zero IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidLex IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd order_zero covariant_swap_add_of_covariant_add WithTop.coe_injective order_eq_orderTop_of_ne_zero orderTop_abs
support_abs 📖	mathematical	—	support SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DFunLike.coe Equiv Lex HahnSeries EquivLike.toFunLike Equiv.instEquivLike ofLex abs instLinearOrderLex instAddGroupLex instAddGroup AddCommGroup.toAddGroup	—	le_total abs_eq_neg_self instIsOrderedAddMonoidLex IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono support_neg abs_eq_self

Pi

Definitions

Name	Category	Theorems
Lex 📖	MathDef	11 math math: lex_eq_dfinsupp_lex, isTrichotomous_lex, DFinsupp.lex_lt_of_lt, lex_iff_of_unique, Finsupp.lex_lt_of_lt, Fin.pi_lex_lt_cons_cons, lex_lt_of_lt, List.Nat.antidiagonalTuple_pairwise_pi_lex, trichotomous_lex, lex_eq_finsupp_lex, Lex.wellFounded

(root)

Definitions

Name	Category	Theorems
Lex 📖	CompOp	415 math math: Prod.Lex.toLex_lt_toLex', HahnEmbedding.IsPartial.baseEmbedding_le, toLex_sub, instIsCancelAddLex, DFinsupp.lex_lt_iff_of_unique, toLex_mul, Sigma.Lex.denselyOrdered_of_noMaxOrder, Lex.forall, Sum.Lex.Icc_inr_inr, PSigma.Lex.denselyOrdered_of_noMinOrder, instIsOrderedCancelAddMonoidLexFinsupp, Pi.Lex.sSup_apply_le, WithBot.orderIsoPUnitSumLex_symm_inl, isLeftRegular_toLex, Lex.exists, OrderIso.sumLexIicIoi_symm_apply_of_lt, Lex.instVAddAssocClass', toLex_inj, HahnSeries.instIsStrictOrderedRingLexOfIsDomain, Prod.Lex.lt_iff', ofLex_symm_eq, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, Prod.Lex.compare_def, Sum.Lex.Ico_inl_inl, Sum.Lex.Ico_inr_inr, MvPowerSeries.exists_finsupp_eq_lexOrder_of_ne_zero, pow_toLex, Sum.Lex.noMaxOrder, toLex_ofNat, Sum.Lex.Ioo_inl_inr, LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex, ofLex_add, toEquiv_toLexMulEquiv, isRightRegular_ofLex, DFinsupp.toLex_monotone, toLex_eq_one, ofLex_ratCast, Lex.instIsScalarTower'', Pi.ofLex_apply, Sum.Lex.inr_le_inr_iff, MvPowerSeries.min_lexOrder_le, Pi.lex_le_iff_of_unique, Lex.instIsScalarTower, WithBot.orderIsoPUnitSumLex_symm_inr, Sum.Lex.Ioo_inr_inl, Pi.instNoMinOrderLexForallOfWellFoundedLTOfNonempty, OrderIso.sumLexIioIci_symm_apply_Ici, Finsupp.Lex.addLeftMono, Finsupp.Lex.single_strictAnti, Sum.Lex.Iic_inr, Sigma.Lex.le_def, ofLex_sub, NonemptyInterval.toLex_strictMono, OrderIso.sumLexAssoc_symm_apply_inr_inr, MvPolynomial.supDegree_esymmAlgHomMonomial, ofLex_intCast, Prod.Lex.monotone_fst_ofLex, isRegular_toLex, Sum.Lex.inr_strictMono, Prod.Lex.toLexOrderHom_coe, HahnEmbedding.Partial.archimedeanClassMk_eq_iff, Prod.Lex.toLex_le_toLex', HahnSeries.support_abs, OrderAddMonoidHom.addCommute_inlₗ_inrₗ, DFinsupp.Lex.isOrderedCancelAddMonoid, HahnEmbedding.Seed.baseEmbedding_strictMono, Prod.Lex.isOrderedAddMonoid, Sum.Lex.Ioo_inr_inr, OrderIso.sumLexCongr_trans, Sum.Lex.noMaxOrder_of_nonempty, DFinsupp.Lex.isOrderedAddMonoid, toLex_vadd', PSigma.Lex.noMaxOrder_of_nonempty, Tuple.monotone_proj, Sum.Lex.inl_bot, Prod.Lex.instDenselyOrderedLex, Lex.instVAddCommClass'', Prod.Lex.prodLexAssoc_symm_apply, OrderType.type_lex_prod, HahnEmbedding.Partial.toOrderAddMonoidHom_apply, MvPowerSeries.lexOrder_def_of_ne_zero, symm_ofLexAddEquiv, Pi.toLex_update_le_self_iff, symm_toLexLinearEquiv, Sum.Lex.toLex_lt_toLex, Pi.toLex_update_lt_self_iff, OrderIso.sumLexIicIoi_symm_apply_of_le, Pi.Lex.sInf_apply, Sigma.Lex.denselyOrdered_of_noMinOrder, instIsCancelMulLex, ofLex_vadd, Finsupp.Lex.isStrictOrder, MvPowerSeries.lexOrder_mul, DFinsupp.lex_lt_iff, HahnEmbedding.Partial.orderTop_eq_iff, ofLex_pow, Lex.instVAddCommClass', Sum.Lex.Icc_inl_inl, Function.Lex.wellFoundedLT, MvPowerSeries.le_lexOrder_iff, Pi.le_toLex_update_self_iff, WithTop.orderIsoSumLexPUnit_toLex, Sum.Lex.inl_mono, MvPolynomial.leadingCoeff_esymmAlgHomMonomial, Prod.Lex.sumLexProdLexDistrib_symm_apply, Sum.Lex.toLexRelIsoLE_coe, ofLex_eq_one, Prod.Lex.instOrientedOrdLex, HahnEmbedding.IsPartial.strictMono, Tuple.graphEquiv₂_apply, WithTop.orderIsoSumLexPUnit_symm_inl, Sum.Lex.Ioi_inr, PSigma.Lex.noMinOrder, DFinsupp.Lex.le_iff_of_unique, HahnSeries.embDomainOrderEmbedding_apply, OrderIso.sumLexIioIci_symm_apply_Iio, Prod.Lex.le_iff, HahnEmbedding.IsPartial.truncLT_mem_range, toLex_ofLex, Sigma.Lex.noMaxOrder_of_nonempty, HahnSeries.order_abs, Sum.Lex.Ici_inl, PSigma.Lex.noMaxOrder, Sum.Lex.Ioc_inl_inl, coe_toLexLinearEquiv, toLex_add, Lex.instVAddCommClass, isAddLeftRegular_toLex, OrderMonoidHom.inrₗ_apply, ofLex_neg, ofLex_natCast, Pi.lex_desc, Sum.Lex.toLex_le_toLex, toLex_pow, coe_ofLexMulEquiv, Finsupp.Lex.single_lt_iff, Sum.Lex.Icc_inr_inl, Prod.Lex.noMaxOrder_of_left, symm_toLexAddEquiv, Tuple.self_comp_sort, OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex, toLex_ratCast, Sum.Lex.Ioc_inl_inr, Prod.Lex.noMinOrder_of_left, Sum.Lex.Iio_inl, Sum.Lex.toLexRelIsoLE_symm_coe, OrderAddMonoidHom.fstₗ_comp_inlₗ, Sum.Lex.denselyOrdered_of_noMaxOrder, toLex_intCast, OrderIso.sumLexIicIoi_symm_apply_Iic, HahnSeries.archimedeanClassMk_eq_archimedeanClassMk_iff, Prod.Lex.sumLexProdLexDistrib_apply, instIsCancelMulZeroLex, isAddRightRegular_toLex, ofLex_toLex, Pi.lex_lt_iff_of_unique, LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ, WithTop.orderIsoSumLexPUnit_top, PSigma.Lex.noMinOrder_of_nonempty, HahnSeries.leadingCoeff_pos_iff, Prod.Lex.uniqueProd_apply, toLex_zero, Sum.Lex.Ioc_inr_inl, OrderIso.sumLexCongr_apply, HahnEmbedding.Partial.eval_smul, MvPolynomial.supDegree_esymm, DFinsupp.Lex.addLeftStrictMono, Prod.Lex.toLex_lt_toLex, Sum.Lex.inr_inf, OrderIso.sumLexIicIoi_symm_apply_Ioi, DFinsupp.Lex.addRightStrictMono, Sum.Lex.Ioc_inr_inr, Prod.Lex.covBy_iff, HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_snd, Finsupp.Lex.le_iff_of_unique, Finsupp.DegLex.lt_iff, Sigma.Lex.noMinOrder, MvPolynomial.leadingCoeff_toLex_C, MvPowerSeries.lexOrder_zero, Pi.Lex.wellFoundedLT, Sum.Lex.Ioi_inl, Finsupp.lex_lt_iff_of_unique, instIsRightCancelMulLex, Sum.Lex.denselyOrdered_of_noMinOrder, Sum.Lex.Ioo_inl_inl, MvPolynomial.monic_esymm, ofLex_one, instLawfulBEqLex, isAddRegular_toLex, Pi.Lex.le_sInf_apply, OrderIso.sumLexIicIoi_apply_inr, instIsLeftCancelMulLex, toLex_natCast, Sum.Lex.Iic_inl, HahnSeries.embDomainOrderAddMonoidHom_injective, Sum.Lex.inl_strictMono, toLex_symm_eq, MvPolynomial.supDegree_toLex_C, Lex.instVAddAssocClass'', isRightRegular_toLex, instNontrivialLex, Prod.Lex.noMinOrder_of_right, toLex_inv, OrderMonoidHom.inlₗ_apply, Sum.Lex.Ici_inr, instNonemptyLex, Sigma.Lex.noMaxOrder, Lex.instSMulCommClass', DFinsupp.Lex.lt_iff_of_unique, OrderIso.sumLexAssoc_symm_apply_inr_inl, Sum.Lex.inl_lt_inl_iff, OrderIso.sumLexAssoc_apply_inl_inl, DFinsupp.Lex.wellFoundedLT_of_finite, Sum.Lex.Ico_inr_inl, toLex_vadd, HahnSeries.archimedeanClassOrderIsoWithTop_apply, OrderAddMonoidHom.inlₗ_apply, OrderMonoidHom.fstₗ_apply, DFinsupp.Lex.addRightMono, Tuple.graph.card, OrderIso.sumLexEmpty_apply_inl, OrderIso.sumLexIicIoi_apply_inl, Pi.Lex.isOrderedAddCancelMonoid, LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ, Sum.Lex.lt_def, isAddRightRegular_ofLex, DFinsupp.Lex.isStrictOrder, Sum.Lex.Ico_inl_inr, Finsupp.Lex.addRightStrictMono, OrderIso.sumLexCongr_refl, Sigma.Lex.denselyOrdered, OrderMonoidHom.commute_inlₗ_inrₗ, ofLex_inj, ofLex_inv, Lex.instIsScalarTower', LinearOrderedCommGroupWithZero.fst_comp_inl, Sum.Lex.Iio_inr, symm_ofLexMulEquiv, instIsLeftCancelMulZeroLex, Sum.Lex.toLexRelIsoLT_coe, coe_ofLexAddEquiv, DFinsupp.lex_le_iff_of_unique, HahnSeries.leadingCoeff_nonneg_iff, Pi.toLex_apply, toEquiv_ofLexMulEquiv, OrderAddMonoidHom.inlₗ_add_inrₗ_eq_toLex, HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk, HahnSeries.iterateEquiv_apply, Pi.Lex.lt_iff_of_unique, Pi.lt_toLex_update_self_iff, hahnEmbedding_isOrderedModule_rat, Finsupp.Lex.addLeftStrictMono, WithBot.orderIsoPUnitSumLex_toLex, instIsLeftCancelAddLex, Prod.Lex.noMaxOrder_of_right, Lex.instVAddAssocClass, Finset.intervalGapsWithin_snd_of_lt, Sigma.Lex.lt_def, ofLex_ofNat, instIsRightCancelMulZeroLex, Finset.intervalGapsWithin_succ_fst_of_lt, HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding, HahnEmbedding.Partial.mem_domain, toLex_smul', Prod.Lex.toLex_mono, OrderIso.emptySumLex_apply_inr, Sum.Lex.inl_lt_inr, HahnSeries.embDomainOrderAddMonoidHom_apply, HahnEmbedding.Seed.mem_domain_baseEmbedding, MvPowerSeries.lexOrder_eq_top_iff_eq_zero, Finsupp.Lex.single_antitone, Finsupp.lex_le_iff_of_unique, OrderIso.sumLexDualAntidistrib_symm_inl, ofLex_smul', HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff, Pi.instDenselyOrderedLexForall, Finsupp.Lex.isOrderedCancelAddMonoid, LinearOrderedCommGroupWithZero.fst_apply, DFinsupp.Lex.addLeftMono, Finset.intervalGapsWithin_fst_of_lt_lt, pow_ofLex, ofLex_vadd', Tuple.eq_sort_iff', OrderIso.sumLexIioIci_symm_apply_of_ge, ofLex_smul, HahnSeries.lt_iff, HahnSeries.instIsOrderedAddMonoidLex, OrderIso.sumLexCongr_symm, Prod.Lex.toLex_covBy_toLex_iff, instNoZeroDivisorsLex, Prod.Lex.isOrderedCancelMonoid, PSigma.Lex.denselyOrdered, coe_toLexMulEquiv, Finsupp.lex_lt_iff, OrderAddMonoidHom.fstₗ_apply, isAddRegular_ofLex, Pi.Lex.isOrderedCancelMonoid, Prod.Lex.toLex_strictMono, PSigma.Lex.denselyOrdered_of_noMaxOrder, NonemptyInterval.toLex_mono, Pi.instNoMaxOrderLexForallOfWellFoundedLTOfNonempty, MonomialOrder.lex_lt_iff, HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_fst, HahnSeries.orderTop_abs, OrderIso.sumLexIioIci_apply_inl, Sum.Lex.inr_mono, WithTop.orderIsoSumLexPUnit_symm_inr, OrderMonoidHom.fstₗ_comp_inlₗ, HahnSeries.instIsOrderedRingLexOfNoZeroDivisors, OrderIso.sumLexAssoc_apply_inr, Prod.Lex.instWellFoundedLTLex, NonemptyInterval.toLex_lt_toLex, Sum.Lex.not_inr_le_inl, DFinsupp.Lex.wellFoundedLT, HVertexOperator.coeff_comp, ofLex_mul, Finsupp.DegLex.le_iff, Sum.Lex.le_def, Finsupp.Lex.wellFoundedLT, HahnEmbedding.Partial.eval_zero, Fintype.card_lex, HahnSeries.finiteArchimedeanClassOrderIso_apply, toEquiv_toLexAddEquiv, toLex_eq_zero, OrderType.type_lex_sum, MonomialOrder.lex_le_iff, Prod.Lex.instTransOrdLex, Prod.Lex.prodUnique_apply, isAddLeftRegular_ofLex, symm_toLexMulEquiv, toLex_div, MvPolynomial.IsSymmetric.antitone_supDegree, isLeftRegular_ofLex, Finsupp.Lex.addRightMono, Prod.Lex.isOrderedMonoid, Sum.Lex.inr_top, MvPolynomial.leadingCoeff_toLex, HahnSeries.leadingCoeff_neg_iff, Prod.Lex.toLex_le_toLex, MvPowerSeries.lexOrder_le_of_coeff_ne_zero, Sigma.Lex.noMinOrder_of_nonempty, Finsupp.toLex_monotone, Sum.Lex.toLexRelIsoLT_symm_coe, Sum.Lex.inl_inf, ofLex_div, Sum.Lex.toLex_strictMono, Prod.Lex.prodLexCongr_apply, Pi.Lex.sSup_apply, Sum.Lex.noMinOrder, Finsupp.Lex.lt_iff, HahnEmbedding.Partial.exists_domain_eq_top, Sum.Lex.inr_sup, Sum.Lex.inr_lt_inr_iff, LinearOrderedCommGroupWithZero.inl_apply, OrderIso.sumLexDualAntidistrib_symm_inr, LinearOrderedCommGroupWithZero.inr_apply, Finsupp.Lex.single_le_iff, OrderIso.sumLexDualAntidistrib_inr, OrderAddMonoidHom.inrₗ_apply, isRegular_ofLex, instIsRightCancelAddLex, ofLex_eq_zero, MvPowerSeries.le_lexOrder_mul, Prod.Lex.lt_iff, Finsupp.DegLex.lt_def, Prod.Lex.prodLexAssoc_apply, Sum.Lex.Icc_inl_inr, HahnEmbedding.Partial.exists_isMax, instRightDistribClassLex, DFinsupp.Lex.total_le, Lex.instSMulCommClass'', OrderIso.sumLexDualAntidistrib_inl, Sum.Lex.noMinOrder_of_nonempty, toLex_smul, HVertexOperator.comp_apply, toLex_one, OrderIso.sumLexAssoc_symm_apply_inl, HahnSeries.leadingCoeff_nonpos_iff, coe_toLexAddEquiv, Pi.Lex.isStrictOrder, Finsupp.Lex.wellFoundedLT_of_finite, OrderIso.sumLexIioIci_apply_inr, HahnEmbedding.Seed.domain_baseEmbedding, OrderIso.sumLexIioIci_symm_apply_of_lt, Tuple.proj_equiv₁', HahnSeries.iterateEquiv_symm_apply, OrderIso.sumLexAssoc_apply_inl_inr, instLeftDistribClassLex, Finsupp.Lex.lt_iff_of_unique, Sum.Lex.toLex_mono, Pi.toLex_strictMono, NonemptyInterval.toLex_le_toLex, Pi.Lex.noMaxOrder', ofLex_zero, toEquiv_ofLexAddEquiv, hahnEmbedding_isOrderedAddMonoid, Sum.Lex.inl_sup, DFinsupp.Lex.lt_iff, MvPowerSeries.lexOrder_mul_ge, toLex_neg, Sum.Lex.not_inr_lt_inl, HahnSeries.leadingCoeff_abs, instIsDomainLex, coe_ofLexLinearEquiv, WithBot.orderIsoPUnitSumLex_bot, Set.PartiallyWellOrderedOn.ProdLex_iff, Lex.instSMulCommClass, Prod.Lex.le_iff', hahnEmbedding_isOrderedModule, symm_ofLexLinearEquiv, Sum.Lex.inl_le_inr, Prod.Lex.isOrderedAddCancelMonoid, Sum.Lex.inl_le_inl_iff, Pi.toLex_monotone, HahnEmbedding.Partial.toOrderAddMonoidHom_injective

---

← Back to Index