Commit 2025-12-17 18:54 4cd85ce2

View on Github →

chore(Algebra/Order/AddGroupWithTop): golf (#32382)

Estimated changes

Modified Mathlib/Algebra/Order/AddGroupWithTop.lean

modified theorem LinearOrderedAddCommGroupWithTop.add_eq_top

added theorem LinearOrderedAddCommGroupWithTop.add_lt_top

added theorem LinearOrderedAddCommGroupWithTop.add_ne_top

added theorem LinearOrderedAddCommGroupWithTop.add_neg_cancel_left_of_ne_top

deleted theorem LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.add_neg_cancel_right_of_ne_top

modified theorem LinearOrderedAddCommGroupWithTop.injective_add_left_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.isAddUnit_iff

added theorem LinearOrderedAddCommGroupWithTop.neg_add_cancel_left_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.neg_add_cancel_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.neg_add_cancel_right_of_ne_top

modified theorem LinearOrderedAddCommGroupWithTop.neg_eq_top

added theorem LinearOrderedAddCommGroupWithTop.sub_top

modified theorem LinearOrderedAddCommGroupWithTop.top_ne_zero

added theorem LinearOrderedAddCommGroupWithTop.top_pos

modified theorem WithTop.LinearOrderedAddCommGroup.coe_neg

modified theorem WithTop.LinearOrderedAddCommGroup.coe_sub

modified theorem WithTop.LinearOrderedAddCommGroup.neg_top

modified theorem WithTop.LinearOrderedAddCommGroup.sub_eq_top_iff

modified theorem WithTop.LinearOrderedAddCommGroup.sub_top

modified theorem WithTop.LinearOrderedAddCommGroup.top_sub

Modified Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

Modified Mathlib/Algebra/Order/Ring/Archimedean.lean