Theorem LinearOrderedAddCommGroupWithTop.injective_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.injective_add_left_of_ne_topView on Github →
2025-12-17 18:54
Mathlib/Algebra/Order/AddGroupWithTop.lean
chore(Algebra/Order/AddGroupWithTop): golf (#32382)
Modified LinearOrderedAddCommGroupWithTop.injective_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.injective_add_left_of_ne_topView on Github →