Theorems · Inductive type · order theory
LinearOrderedAddCommMonoidWithTop
Type u_3 → Type u_3
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
- Cited by
- 68 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by85
Results whose statement or proof uses this declaration.
- AddValuationstatement and proof · cited by 96
- top_addstatement and proof · cited by 55
- add_topstatement and proof · cited by 49
- AddValuation.toValuationstatement and proof · cited by 21
- AddValuation.IsEquivstatement and proof · cited by 8
- AddValuation.comapstatement and proof · cited by 7
- AddValuation.suppstatement and proof · cited by 7
- AddValuation.map_mulstatement and proof · cited by 5
- AddValuation.map_powstatement and proof · cited by 5
- AddValuation.map_zerostatement and proof · cited by 5
- AddValuation.ofValuationstatement and proof · cited by 5
- add_right_injective_of_ne_topstatement and proof · cited by 3