AddGroupWithTop

📁 Source: Mathlib/Algebra/Order/AddGroupWithTop.lean

Statistics

Metric	Count
Definitions `LinearOrderedAddCommGroupWithTop`, `instLinearOrderedAddCommMonoidWithTop`, `toAddCommMonoid`, `toLinearOrder`, `toNeg`, `toOrderTop`, `toSub`, `toSubNegMonoid`, `toSubtractionMonoid`, `zsmul`, `LinearOrderedAddCommMonoidWithTop`, `toAddCommMonoid`, `toLinearOrder`, `toOrderTop`, `instLinearOrderedAddCommGroupWithTopOfIsOrderedAddMonoid`, `instNeg`, `instSub`, `linearOrderedAddCommMonoidWithTop`	18
Theorems `of_ne_top`, `add_eq_top`, `add_lt_top`, `add_ne_top`, `add_neg_cancel`, `add_neg_cancel_iff_ne_top`, `add_neg_cancel_left_of_ne_top`, `add_neg_cancel_of_ne_top`, `add_neg_cancel_right_of_ne_top`, `injective_add_left_of_ne_top`, `injective_add_right_of_ne_top`, `isAddUnit_iff`, `neg_add_cancel_left_of_ne_top`, `neg_add_cancel_of_ne_top`, `neg_add_cancel_right_of_ne_top`, `neg_eq_top`, `neg_pos`, `neg_top`, `strictMono_add_left_of_ne_top`, `strictMono_add_right_of_ne_top`, `sub_eq_add_neg`, `sub_eq_zero`, `sub_le_sub_iff_left_of_ne_top`, `sub_left_inj_of_ne_top`, `sub_left_injective_of_ne_top`, `sub_left_strictMono_of_ne_top`, `sub_lt_sub_iff_left_of_ne_top`, `sub_pos`, `sub_right_inj_of_ne_top`, `sub_right_injective_of_ne_top`, `sub_self_eq_zero_iff_ne_top`, `sub_self_eq_zero_of_ne_top`, `sub_self_nonneg`, `sub_top`, `toIsOrderedAddMonoid`, `toNontrivial`, `top_add'`, `top_ne_zero`, `top_pos`, `zero_ne_top`, `zsmul_neg'`, `zsmul_succ'`, `zsmul_zero'`, `isAddLeftRegular_of_ne_top`, `toIsOrderedAddMonoid`, `top_add'`, `coe_neg`, `coe_sub`, `neg_top`, `sub_eq_top_iff`, `sub_top`, `top_sub`, `add_le_add_iff_left_of_ne_top`, `add_le_add_iff_right_of_ne_top`, `add_left_inj_of_ne_top`, `add_left_injective_of_ne_top`, `add_left_strictMono_of_ne_top`, `add_lt_add_iff_left_of_ne_top`, `add_lt_add_iff_right_of_ne_top`, `add_right_inj_of_ne_top`, `add_right_injective_of_ne_top`, `add_right_strictMono_of_ne_top`, `add_top`, `top_add`	64
Total	82

IsAddRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_ne_top` 📖	mathematical	—	`IsAddRegular` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid`	—	`LinearOrderedAddCommMonoidWithTop.isAddLeftRegular_of_ne_top`

LinearOrderedAddCommGroupWithTop

Definitions

Name	Category	Theorems
`instLinearOrderedAddCommMonoidWithTop` 📖	CompOp	2 math math: `AddValuation.map_div`, `AddValuation.map_inv`
`toAddCommMonoid` 📖	CompOp	15 math math: `neg_add_cancel_right_of_ne_top`, `add_eq_top`, `add_neg_cancel_right_of_ne_top`, `neg_add_cancel_of_ne_top`, `add_neg_cancel`, `zsmul_succ'`, `add_neg_cancel_iff_ne_top`, `sub_eq_add_neg`, `add_lt_top`, `add_neg_cancel_left_of_ne_top`, `toIsOrderedAddMonoid`, `zsmul_zero'`, `neg_add_cancel_left_of_ne_top`, `top_add'`, `add_neg_cancel_of_ne_top`
`toLinearOrder` 📖	CompOp	14 math math: `neg_eq_top`, `sub_pos`, `add_eq_top`, `sub_top`, `neg_pos`, `sub_left_strictMono_of_ne_top`, `top_pos`, `add_lt_top`, `neg_top`, `toIsOrderedAddMonoid`, `sub_le_sub_iff_left_of_ne_top`, `sub_self_nonneg`, `top_add'`, `sub_lt_sub_iff_left_of_ne_top`
`toNeg` 📖	CompOp	5 math math: `add_neg_cancel`, `sub_eq_add_neg`, `neg_top`, `zsmul_neg'`, `add_neg_cancel_of_ne_top`
`toOrderTop` 📖	CompOp	9 math math: `neg_eq_top`, `sub_pos`, `add_eq_top`, `sub_top`, `neg_pos`, `top_pos`, `add_lt_top`, `neg_top`, `top_add'`
`toSub` 📖	CompOp	1 math math: `sub_eq_add_neg`
`toSubNegMonoid` 📖	CompOp	24 math math: `neg_eq_top`, `sub_pos`, `sub_self_eq_zero_iff_ne_top`, `neg_add_cancel_right_of_ne_top`, `add_neg_cancel_right_of_ne_top`, `neg_add_cancel_of_ne_top`, `sub_right_injective_of_ne_top`, `sub_top`, `ArchimedeanClass.FiniteElement.mk_mul_mk`, `sub_left_strictMono_of_ne_top`, `top_pos`, `sub_left_inj_of_ne_top`, `add_neg_cancel_left_of_ne_top`, `sub_left_injective_of_ne_top`, `sub_eq_zero`, `neg_add_cancel_left_of_ne_top`, `sub_self_eq_zero_of_ne_top`, `isAddUnit_iff`, `AddValuation.map_div`, `sub_le_sub_iff_left_of_ne_top`, `sub_self_nonneg`, `ArchimedeanClass.mk_div`, `sub_right_inj_of_ne_top`, `sub_lt_sub_iff_left_of_ne_top`
`toSubtractionMonoid` 📖	CompOp	8 math math: `sub_pos`, `sub_self_eq_zero_iff_ne_top`, `add_neg_cancel_iff_ne_top`, `neg_pos`, `sub_eq_zero`, `sub_self_eq_zero_of_ne_top`, `sub_self_nonneg`, `AddValuation.map_inv`
`zsmul` 📖	CompOp	3 math math: `zsmul_succ'`, `zsmul_neg'`, `zsmul_zero'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_eq_top` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `toAddCommMonoid` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `toLinearOrder` `toOrderTop`	—	`not_iff_not` `add_ne_top`
`add_lt_top` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `toLinearOrder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `toAddCommMonoid` `Top.top` `OrderTop.toTop` `Preorder.toLE` `LinearOrder.toPartialOrder` `toOrderTop`	—	—
`add_ne_top` 📖	—	—	—	—	`instIsDedekindFiniteAddMonoid`
`add_neg_cancel` 📖	mathematical	—	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `toAddCommMonoid` `toNeg` `AddMonoid.toZero`	—	`add_neg_cancel_of_ne_top`
`add_neg_cancel_iff_ne_top` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `toAddCommMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `toSubtractionMonoid` `NegZeroClass.toZero`	—	`Mathlib.Tactic.Contrapose.contrapose₃` `neg_top` `add_top` `add_neg_cancel_of_ne_top`
`add_neg_cancel_left_of_ne_top` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `toAddCommMonoid` `SubNegMonoid.toNeg` `toSubNegMonoid`	—	`add_neg_cancel_of_ne_top` `zero_add`
`add_neg_cancel_of_ne_top` 📖	mathematical	—	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `toAddCommMonoid` `toNeg` `AddMonoid.toZero`	—	—
`add_neg_cancel_right_of_ne_top` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `toAddCommMonoid` `SubNegMonoid.toNeg` `toSubNegMonoid`	—	`add_assoc` `add_neg_cancel_of_ne_top` `add_zero`
`injective_add_left_of_ne_top` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid`	—	`add_left_injective_of_ne_top`
`injective_add_right_of_ne_top` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid`	—	`add_right_injective_of_ne_top`
`isAddUnit_iff` 📖	mathematical	—	`IsAddUnit` `SubNegMonoid.toAddMonoid` `toSubNegMonoid`	—	`top_add'` `IsAddUnit.of_add_eq_zero` `instIsDedekindFiniteAddMonoid` `add_neg_cancel_of_ne_top`
`neg_add_cancel_left_of_ne_top` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `toAddCommMonoid` `SubNegMonoid.toNeg` `toSubNegMonoid`	—	`neg_add_cancel_of_ne_top` `zero_add`
`neg_add_cancel_of_ne_top` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `toAddCommMonoid` `SubNegMonoid.toNeg` `toSubNegMonoid` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid`	—	`add_comm` `add_neg_cancel_of_ne_top`
`neg_add_cancel_right_of_ne_top` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `toAddCommMonoid` `SubNegMonoid.toNeg` `toSubNegMonoid`	—	`add_assoc` `neg_add_cancel_of_ne_top` `add_zero`
`neg_eq_top` 📖	mathematical	—	`SubNegMonoid.toNeg` `toSubNegMonoid` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `toLinearOrder` `toOrderTop`	—	`add_top` `add_neg_cancel_of_ne_top` `neg_top`
`neg_pos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `toLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `toSubtractionMonoid` `NegZeroClass.toNeg` `Top.top` `OrderTop.toTop` `Preorder.toLE` `LinearOrder.toPartialOrder` `toOrderTop`	—	`zero_sub` `sub_pos`
`neg_top` 📖	mathematical	—	`toNeg` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `toLinearOrder` `toOrderTop`	—	—
`strictMono_add_left_of_ne_top` 📖	mathematical	—	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedAddCommMonoidWithTop.toLinearOrder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid`	—	`add_left_strictMono_of_ne_top`
`strictMono_add_right_of_ne_top` 📖	mathematical	—	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedAddCommMonoidWithTop.toLinearOrder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid`	—	`add_right_strictMono_of_ne_top`
`sub_eq_add_neg` 📖	mathematical	—	`toSub` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `toAddCommMonoid` `toNeg`	—	—
`sub_eq_zero` 📖	mathematical	—	`SubNegMonoid.toSub` `toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `toSubtractionMonoid`	—	`sub_self_eq_zero_of_ne_top` `sub_left_inj_of_ne_top`
`sub_le_sub_iff_left_of_ne_top` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `toLinearOrder` `SubNegMonoid.toSub` `toSubNegMonoid`	—	`StrictMono.le_iff_le` `sub_left_strictMono_of_ne_top`
`sub_left_inj_of_ne_top` 📖	mathematical	—	`SubNegMonoid.toSub` `toSubNegMonoid`	—	`sub_left_injective_of_ne_top`
`sub_left_injective_of_ne_top` 📖	mathematical	—	`SubNegMonoid.toSub` `toSubNegMonoid`	—	`sub_eq_add_neg` `add_left_injective_of_ne_top`
`sub_left_strictMono_of_ne_top` 📖	mathematical	—	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `toLinearOrder` `SubNegMonoid.toSub` `toSubNegMonoid`	—	`sub_eq_add_neg` `add_left_strictMono_of_ne_top`
`sub_lt_sub_iff_left_of_ne_top` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `toLinearOrder` `SubNegMonoid.toSub` `toSubNegMonoid`	—	`StrictMono.lt_iff_lt` `sub_left_strictMono_of_ne_top`
`sub_pos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `toLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `toSubtractionMonoid` `SubNegMonoid.toSub` `toSubNegMonoid` `Top.top` `OrderTop.toTop` `Preorder.toLE` `LinearOrder.toPartialOrder` `toOrderTop`	—	`eq_or_ne` `sub_top` `sub_self_eq_zero_of_ne_top`
`sub_right_inj_of_ne_top` 📖	mathematical	—	`SubNegMonoid.toSub` `toSubNegMonoid`	—	`sub_right_injective_of_ne_top`
`sub_right_injective_of_ne_top` 📖	mathematical	—	`SubNegMonoid.toSub` `toSubNegMonoid`	—	`sub_eq_add_neg` `add_right_injective_of_ne_top` `neg_injective`
`sub_self_eq_zero_iff_ne_top` 📖	mathematical	—	`SubNegMonoid.toSub` `toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `toSubtractionMonoid`	—	`sub_eq_add_neg` `add_neg_cancel_iff_ne_top`
`sub_self_eq_zero_of_ne_top` 📖	mathematical	—	`SubNegMonoid.toSub` `toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `toSubtractionMonoid`	—	`sub_self_eq_zero_iff_ne_top`
`sub_self_nonneg` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `toLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `toSubtractionMonoid` `SubNegMonoid.toSub` `toSubNegMonoid`	—	`eq_or_ne` `sub_top` `sub_self_eq_zero_of_ne_top` `le_refl`
`sub_top` 📖	mathematical	—	`SubNegMonoid.toSub` `toSubNegMonoid` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `toLinearOrder` `toOrderTop`	—	`sub_eq_add_neg` `neg_top` `add_top`
`toIsOrderedAddMonoid` 📖	mathematical	—	`IsOrderedAddMonoid` `toAddCommMonoid` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `toLinearOrder`	—	—
`toNontrivial` 📖	mathematical	—	`Nontrivial`	—	—
`top_add'` 📖	mathematical	—	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `toAddCommMonoid` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `toLinearOrder` `toOrderTop`	—	—
`top_ne_zero` 📖	—	—	—	—	`exists_ne` `toNontrivial` `top_add'` `zero_add`
`top_pos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `toLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `toSubNegMonoid` `Top.top` `OrderTop.toTop` `Preorder.toLE` `LinearOrder.toPartialOrder` `toOrderTop`	—	`lt_top_iff_ne_top` `top_ne_zero`
`zero_ne_top` 📖	—	—	—	—	`top_ne_zero`
`zsmul_neg'` 📖	mathematical	—	`zsmul` `toNeg`	—	—
`zsmul_succ'` 📖	mathematical	—	`zsmul` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `toAddCommMonoid`	—	—
`zsmul_zero'` 📖	mathematical	—	`zsmul` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `toAddCommMonoid`	—	—

LinearOrderedAddCommMonoidWithTop

Definitions

Name	Category	Theorems
`toAddCommMonoid` 📖	CompOp	44 math math: `add_right_strictMono_of_ne_top`, `AddValuation.map_pow`, `AddValuation.map_apply`, `add_right_injective_of_ne_top`, `Finset.set_encard_biUnion_le`, `Finset.emultiplicity_prod`, `ENat.iInf_sum`, `add_top`, `ENat.sum_iSup`, `add_left_strictMono_of_ne_top`, `Set.encard_iUnion_of_finite`, `ENat.sum_lt_top`, `toIsOrderedAddMonoid`, `LinearOrderedAddCommGroupWithTop.injective_add_right_of_ne_top`, `LinearOrderedAddCommGroupWithTop.strictMono_add_left_of_ne_top`, `MvPowerSeries.le_weightedOrder_subst`, `add_le_add_iff_left_of_ne_top`, `add_lt_add_iff_left_of_ne_top`, `Set.encard_iUnion_le_of_finite`, `AddValuation.map_mul`, `isAddLeftRegular_of_ne_top`, `add_left_injective_of_ne_top`, `PowerSeries.order_prod`, `IsAddRegular.of_ne_top`, `Module.length_pi_of_fintype`, `top_add`, `top_add'`, `ENat.sum_eq_top`, `ENat.sum_lt_sum_of_nonempty`, `Set.Finite.encard_biUnion`, `MvPowerSeries.order_prod`, `ENat.sum_iSup_of_monotone`, `LinearOrderedAddCommGroupWithTop.strictMono_add_right_of_ne_top`, `add_left_inj_of_ne_top`, `add_right_inj_of_ne_top`, `Set.encard_iUnion_le_of_fintype`, `AddValuation.map_one`, `Set.Finite.encard_biUnion_le`, `PowerSeries.le_order_prod`, `ENat.toNat_sum`, `LinearOrderedAddCommGroupWithTop.injective_add_left_of_ne_top`, `add_lt_add_iff_right_of_ne_top`, `MvPowerSeries.weightedOrder_prod`, `add_le_add_iff_right_of_ne_top`
`toLinearOrder` 📖	CompOp	29 math math: `ofDual_toAdd_zero`, `add_right_strictMono_of_ne_top`, `AddValuation.top_iff`, `AddValuation.map_add'`, `add_top`, `AddValuation.map_le_add`, `AddValuation.map_add_of_distinct_val`, `AddValuation.map_lt_sum`, `add_left_strictMono_of_ne_top`, `ofAdd_bot`, `toIsOrderedAddMonoid`, `LinearOrderedAddCommGroupWithTop.strictMono_add_left_of_ne_top`, `AddValuation.map_zero`, `add_le_add_iff_left_of_ne_top`, `add_lt_add_iff_left_of_ne_top`, `AddValuation.map_lt_add`, `AddValuation.map_sub`, `ofDual_toAdd_eq_top_iff`, `top_add`, `top_add'`, `AddValuation.map_le_sub`, `AddValuation.mem_supp_iff`, `LinearOrderedAddCommGroupWithTop.strictMono_add_right_of_ne_top`, `AddValuation.map_lt_sum'`, `AddValuation.map_add`, `ofAdd_toDual_eq_zero_iff`, `add_lt_add_iff_right_of_ne_top`, `AddValuation.map_le_sum`, `add_le_add_iff_right_of_ne_top`
`toOrderTop` 📖	CompOp	10 math math: `ofDual_toAdd_zero`, `AddValuation.top_iff`, `add_top`, `ofAdd_bot`, `AddValuation.map_zero`, `ofDual_toAdd_eq_top_iff`, `top_add`, `top_add'`, `AddValuation.mem_supp_iff`, `ofAdd_toDual_eq_zero_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddLeftRegular_of_ne_top` 📖	mathematical	—	`IsAddLeftRegular` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `toAddCommMonoid`	—	—
`toIsOrderedAddMonoid` 📖	mathematical	—	`IsOrderedAddMonoid` `toAddCommMonoid` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `toLinearOrder`	—	—
`top_add'` 📖	mathematical	—	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `toAddCommMonoid` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `toLinearOrder` `toOrderTop`	—	—

WithTop

Definitions

Name	Category	Theorems
`linearOrderedAddCommMonoidWithTop` 📖	CompOp	4 math math: `Padic.addValuation.apply`, `HahnSeries.addVal_le_of_coeff_ne_zero`, `HahnSeries.addVal_apply_of_ne`, `HahnSeries.addVal_apply`

WithTop.LinearOrderedAddCommGroup

Definitions

Name	Category	Theorems
`instLinearOrderedAddCommGroupWithTopOfIsOrderedAddMonoid` 📖	CompOp	—
`instNeg` 📖	CompOp	7 math math: `Complex.meromorphicOrderAt_canonicalFactor`, `meromorphicOrderAt_inv`, `PeriodPair.order_weierstrassP`, `coe_neg`, `neg_top`, `fun_meromorphicOrderAt_inv`, `WithTop.untop₀_neg`
`instSub` 📖	CompOp	6 math math: `fun_meromorphicOrderAt_div`, `sub_top`, `sub_eq_top_iff`, `meromorphicOrderAt_div`, `top_sub`, `coe_sub`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_neg` 📖	mathematical	—	`WithTop.some` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `WithTop` `instNeg`	—	—
`coe_sub` 📖	mathematical	—	`WithTop.some` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `WithTop` `instSub`	—	—
`neg_top` 📖	mathematical	—	`WithTop` `instNeg` `Top.top` `WithTop.top`	—	—
`sub_eq_top_iff` 📖	mathematical	—	`WithTop` `instSub` `Top.top` `WithTop.top`	—	`sub_top` `top_sub`
`sub_top` 📖	mathematical	—	`WithTop` `instSub` `Top.top` `WithTop.top`	—	—
`top_sub` 📖	mathematical	—	`WithTop` `instSub` `Top.top` `WithTop.top`	—	—

(root)

Definitions

Name	Category	Theorems
`LinearOrderedAddCommGroupWithTop` 📖	CompData	—
`LinearOrderedAddCommMonoidWithTop` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_le_add_iff_left_of_ne_top` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedAddCommMonoidWithTop.toLinearOrder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid`	—	`StrictMono.le_iff_le` `add_left_strictMono_of_ne_top`
`add_le_add_iff_right_of_ne_top` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedAddCommMonoidWithTop.toLinearOrder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid`	—	`StrictMono.le_iff_le` `add_right_strictMono_of_ne_top`
`add_left_inj_of_ne_top` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid`	—	`add_left_injective_of_ne_top`
`add_left_injective_of_ne_top` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid`	—	`IsAddRegular.right` `IsAddRegular.of_ne_top`
`add_left_strictMono_of_ne_top` 📖	mathematical	—	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedAddCommMonoidWithTop.toLinearOrder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid`	—	`Monotone.strictMono_of_injective` `add_left_mono` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `add_left_injective_of_ne_top`
`add_lt_add_iff_left_of_ne_top` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedAddCommMonoidWithTop.toLinearOrder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid`	—	`StrictMono.lt_iff_lt` `add_left_strictMono_of_ne_top`
`add_lt_add_iff_right_of_ne_top` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedAddCommMonoidWithTop.toLinearOrder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid`	—	`StrictMono.lt_iff_lt` `add_right_strictMono_of_ne_top`
`add_right_inj_of_ne_top` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid`	—	`add_right_injective_of_ne_top`
`add_right_injective_of_ne_top` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid`	—	`IsAddRegular.left` `IsAddRegular.of_ne_top`
`add_right_strictMono_of_ne_top` 📖	mathematical	—	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedAddCommMonoidWithTop.toLinearOrder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid`	—	`Monotone.strictMono_of_injective` `add_right_mono` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `add_right_injective_of_ne_top`
`add_top` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `LinearOrderedAddCommMonoidWithTop.toLinearOrder` `LinearOrderedAddCommMonoidWithTop.toOrderTop`	—	`add_comm` `top_add`
`top_add` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `LinearOrderedAddCommMonoidWithTop.toLinearOrder` `LinearOrderedAddCommMonoidWithTop.toOrderTop`	—	`LinearOrderedAddCommMonoidWithTop.top_add'`

---

← Back to Index