Commit 2025-01-04 06:32 e71f6e97

View on Github →

feat(Algebra/Order/AddGroupWithTop): lemmas about LinearOrderedAddCommGroupWithTop (#18954)

Estimated changes

Modified Mathlib/Algebra/Order/AddGroupWithTop.lean

added theorem LinearOrderedAddCommGroupWithTop.injective_add_left_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.injective_add_right_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.strictMono_add_left_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.strictMono_add_right_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.sub_pos