Commit 2025-12-29 13:42 e7c9f118

View on Github →

feat(Algebra/Order/AddGroupWithTop): more monotonicity/injectivity lemmas (#33349) We also deprecate some injective_foo lemmas in favor of foo_injective counterparts, as per the naming conventions.

Estimated changes

Modified Mathlib/Algebra/Order/AddGroupWithTop.lean

added theorem LinearOrderedAddCommGroupWithTop.add_le_add_iff_left_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.add_le_add_iff_right_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.add_left_inj_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.add_left_injective_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.add_left_strictMono_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.add_lt_add_iff_left_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.add_lt_add_iff_right_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.add_right_inj_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.add_right_injective_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.add_right_strictMono_of_ne_top

deleted theorem LinearOrderedAddCommGroupWithTop.injective_add_left_of_ne_top

deleted theorem LinearOrderedAddCommGroupWithTop.injective_add_right_of_ne_top

deleted theorem LinearOrderedAddCommGroupWithTop.strictMono_add_left_of_ne_top

deleted theorem LinearOrderedAddCommGroupWithTop.strictMono_add_right_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.sub_le_sub_iff_left_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.sub_left_inj_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.sub_left_injective_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.sub_left_strictMono_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.sub_lt_sub_iff_left_of_ne_top

modified theorem LinearOrderedAddCommGroupWithTop.sub_pos

added theorem LinearOrderedAddCommGroupWithTop.sub_right_inj_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.sub_right_injective_of_ne_top