Structures · Algebra
LinearOrderedAddCommMonoidWithTop
A linearly ordered commutative monoid 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 top_add', isAddLeftRegular_of_ne_top
Extends4
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances7
- ENNReal
- ENat
- ArchimedeanClass
- OrderDual
- PUnit
- WithTop
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by84
- AddValuation
- top_add
- add_top
- AddValuation.toValuation
- AddValuation.IsEquiv
- AddValuation.supp
- AddValuation.comap
- AddValuation.map_pow
- AddValuation.ofValuation
- AddValuation.map_mul
- AddValuation.map_zero
- IsAddRegular.of_ne_top
- add_left_injective_of_ne_top
- add_left_strictMono_of_ne_top
- add_right_injective_of_ne_top
- AddValuation.onQuot
- add_right_strictMono_of_ne_top
- AddValuation.map
- AddValuation.of
- AddValuation.map_add
- AddValuation.map_add_eq_of_lt_left
- LinearOrderedAddCommMonoidWithTop.top_add'
- AddValuation.of_apply
- AddValuation.self_le_supp_comap
- AddValuation.map_sub_swap
- AddValuation.map_neg
- AddValuation.map_one
- AddValuation.map_add_of_distinct_val
- LinearOrderedAddCommMonoidWithTop.isAddLeftRegular_of_ne_top
- AddValuation.map_sub_eq_of_lt_left
- LinearOrderedAddCommMonoidWithTop.toAddCommMonoid
- LinearOrderedAddCommMonoidWithTop.toOrderTop
- add_lt_add_iff_right_of_ne_top
- AddValuation.map_eq_of_lt_sub
- AddValuation.map_le_sum
- ofDual_toAdd_zero
- AddValuation.ofValuation_symm_eq
- add_le_add_iff_left_of_ne_top
- add_lt_add_iff_left_of_ne_top
- AddValuation.IsEquiv.refl
- AddValuation.map_sub_eq_of_lt_right
- AddValuation.IsEquiv.symm
- add_left_inj_of_ne_top
- AddValuation.onQuot_comap_eq
- AddValuation.toValuation_symm_eq
- AddValuation.map_sub
- AddValuation.map_lt_add
- AddValuation.comap_onQuot_eq
- AddValuation.ofValuation_apply
- AddValuation.toPreorder
Ancestors39
- Add
- AddAction
- AddCommMagma
- AddCommMonoid
- AddCommSemigroup
- AddMonoid
- AddSemigroup
- AddSemigroupAction
- AddZero
- AddZeroClass
- DistribLattice
- GradeBoundedOrder
- GradeMaxOrder
- GradeMinOrder
- GradeOrder
- HAdd
- HVAdd
- IsOrderedAddMonoid
- LE
- LT
- Lattice
- Lean.Grind.AddCommMonoid
- Lean.Grind.NatModule
- LinearOrder
- Max
- Min
- NSMul
- Nonempty
- OfNat
- One
- Ord
- OrderTop
- PartialOrder
- Preorder
- SemilatticeInf
- SemilatticeSup
- Top
- VAdd
- Zero