Theorems · Inductive type · order theory
LinearOrderedAddCommGroupWithTop
Type u_3 → Type u_3
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
- Cited by
- 37 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 by46
Results whose statement or proof uses this declaration.
- LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_topstatement and proof · cited by 6
- LinearOrderedAddCommGroupWithTop.neg_topstatement and proof · cited by 5
- LinearOrderedAddCommGroupWithTop.toNegstatement and proof · cited by 4
- LinearOrderedAddCommGroupWithTop.sub_self_eq_zero_of_ne_topstatement and proof · cited by 3
- LinearOrderedAddCommGroupWithTop.toZSMulstatement and proof · cited by 3
- LinearOrderedAddCommGroupWithTop.neg_add_cancel_of_ne_topstatement and proof · cited by 2
- LinearOrderedAddCommGroupWithTop.sub_left_strictMono_of_ne_topstatement and proof · cited by 2
- LinearOrderedAddCommGroupWithTop.sub_topstatement and proof · cited by 2
- LinearOrderedAddCommGroupWithTop.top_add'statement and proof · cited by 2
- LinearOrderedAddCommGroupWithTop.top_ne_zerostatement and proof · cited by 2
- LinearOrderedAddCommGroupWithTop.add_ne_topstatement and proof · cited by 1
- LinearOrderedAddCommGroupWithTop.add_neg_cancel_iff_ne_topstatement and proof · cited by 1