Theorem LinearOrderedAddCommGroupWithTop.sub_left_strictMono_of_ne_top

Modification history

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