Theorem LinearOrderedAddCommGroupWithTop.strictMono_add_left_of_ne_top

Modification history

2025-12-29 13:42
Mathlib/Algebra/Order/AddGroupWithTop.lean
feat(Algebra/Order/AddGroupWithTop): more monotonicity/injectivity lemmas (#33349) …
Deleted LinearOrderedAddCommGroupWithTop.strictMono_add_left_of_ne_topView on Github →
2025-01-04 06:32
Mathlib/Algebra/Order/AddGroupWithTop.lean
feat(Algebra/Order/AddGroupWithTop): lemmas about LinearOrderedAddCommGroupWithTop (#18954)
Added LinearOrderedAddCommGroupWithTop.strictMono_add_left_of_ne_topView on Github →