Structures · Algebra
LinearOrderedAddCommGroupWithTop
A linearly ordered commutative group with an additively absorbing ⊤ element.
Instances should include number systems with an infinite element adjoined.
- Defined in
- Mathlib.Algebra.Order.AddGroupWithTop
- Shape
- One type argument · adds sub_eq_add_neg, zsmul_zero', zsmul_succ', zsmul_neg', top_add', neg_top, add_neg_cancel_of_ne_top
Extends6
Extended by0
Nothing extends this class yet.
Forgetful instances
Every LinearOrderedAddCommGroupWithTop is also a
Concrete types that are instances4
- ArchimedeanClass
- OrderDual
- WithTop
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by49
- LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_top
- LinearOrderedAddCommGroupWithTop.neg_top
- LinearOrderedAddCommGroupWithTop.toNeg
- LinearOrderedAddCommGroupWithTop.sub_self_eq_zero_of_ne_top
- LinearOrderedAddCommGroupWithTop.toZSMul
- LinearOrderedAddCommGroupWithTop.sub_top
- LinearOrderedAddCommGroupWithTop.neg_add_cancel_of_ne_top
- LinearOrderedAddCommGroupWithTop.sub_left_strictMono_of_ne_top
- LinearOrderedAddCommGroupWithTop.top_ne_zero
- LinearOrderedAddCommGroupWithTop.top_add'
- LinearOrderedAddCommGroupWithTop.sub_right_injective_of_ne_top
- LinearOrderedAddCommGroupWithTop.add_ne_top
- LinearOrderedAddCommGroupWithTop.sub_pos
- LinearOrderedAddCommGroupWithTop.sub_left_injective_of_ne_top
- LinearOrderedAddCommGroupWithTop.sub_self_eq_zero_iff_ne_top
- LinearOrderedAddCommGroupWithTop.toSub
- LinearOrderedAddCommGroupWithTop.sub_left_inj_of_ne_top
- LinearOrderedAddCommGroupWithTop.add_neg_cancel_iff_ne_top
- LinearOrderedAddCommGroupWithTop.neg_eq_top
- LinearOrderedAddCommGroupWithTop.sub_le_sub_iff_left_of_ne_top
- LinearOrderedAddCommGroupWithTop.instLinearOrderedAddCommMonoidWithTop
- LinearOrderedAddCommGroupWithTop.neg_pos
- LinearOrderedAddCommGroupWithTop.sub_lt_sub_iff_left_of_ne_top
- LinearOrderedAddCommGroupWithTop.zsmul_succ'
- instLinearOrderedCommGroupWithZeroMultiplicativeOrderDualOfLinearOrderedAddCommGroupWithTop
- LinearOrderedAddCommGroupWithTop.zsmul_neg'
- LinearOrderedAddCommGroupWithTop.toAddCommMonoid
- LinearOrderedAddCommGroupWithTop.sub_self_nonneg
- LinearOrderedAddCommGroupWithTop.sub_right_inj_of_ne_top
- LinearOrderedAddCommGroupWithTop.toSubtractionMonoid
- LinearOrderedAddCommGroupWithTop.isAddUnit_iff
- LinearOrderedAddCommGroupWithTop.neg_add_cancel_right_of_ne_top
- LinearOrderedAddCommGroupWithTop.zero_ne_top
- LinearOrderedAddCommGroupWithTop.toOrderTop
- AddValuation.map_inv
- LinearOrderedAddCommGroupWithTop.sub_eq_zero
- AddValuation.map_div
- LinearOrderedAddCommGroupWithTop.zsmul_zero'
- LinearOrderedAddCommGroupWithTop.toIsOrderedAddMonoid
- LinearOrderedAddCommGroupWithTop.neg_add_cancel_left_of_ne_top
- LinearOrderedAddCommGroupWithTop.add_neg_cancel_left_of_ne_top
- LinearOrderedAddCommGroupWithTop.add_lt_top
- LinearOrderedAddCommGroupWithTop.toSubNegMonoid
- LinearOrderedAddCommGroupWithTop.toLinearOrder
- LinearOrderedAddCommGroupWithTop.top_pos
- LinearOrderedAddCommGroupWithTop.toNontrivial
- LinearOrderedAddCommGroupWithTop.add_eq_top
- LinearOrderedAddCommGroupWithTop.sub_eq_add_neg
- LinearOrderedAddCommGroupWithTop.add_neg_cancel_right_of_ne_top
Ancestors50
- Add
- AddAction
- AddCommMagma
- AddCommMonoid
- AddCommSemigroup
- AddMonoid
- AddSemigroup
- AddSemigroupAction
- AddZero
- AddZeroClass
- DistribLattice
- GradeBoundedOrder
- GradeMaxOrder
- GradeMinOrder
- GradeOrder
- HAdd
- HSub
- HVAdd
- InvolutiveNeg
- IsOrderedAddMonoid
- LE
- LT
- Lattice
- Lean.Grind.AddCommMonoid
- Lean.Grind.NatModule
- LinearOrder
- LinearOrderedAddCommMonoidWithTop
- Max
- Min
- NSMul
- Neg
- NegZeroClass
- Nonempty
- Nontrivial
- OfNat
- One
- Ord
- OrderTop
- PartialOrder
- Preorder
- SemilatticeInf
- SemilatticeSup
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionMonoid
- Top
- VAdd
- ZSMul
- Zero