Theorem LinearOrderedAddCommGroupWithTop.sub_pos

Modification history

2026-01-08 11:26
Mathlib/Algebra/Order/AddGroupWithTop.lean
refactor: make `LinearOrderedCommMonoidWithZero`s cancellative (#31749) …
Modified LinearOrderedAddCommGroupWithTop.sub_posView on Github →
2025-12-29 13:42
Mathlib/Algebra/Order/AddGroupWithTop.lean
feat(Algebra/Order/AddGroupWithTop): more monotonicity/injectivity lemmas (#33349) …
Modified LinearOrderedAddCommGroupWithTop.sub_posView on Github →
2025-01-04 06:32
Mathlib/Algebra/Order/AddGroupWithTop.lean
feat(Algebra/Order/AddGroupWithTop): lemmas about LinearOrderedAddCommGroupWithTop (#18954)
Added LinearOrderedAddCommGroupWithTop.sub_posView on Github →