Commit 2024-11-06 04:34 9c5f3358

View on Github →

feat: SubtractionMonoid instance for LinearOrderedAddCommGroupWithTop (#18665)

Estimated changes

Modified Mathlib/Algebra/Order/AddGroupWithTop.lean

added theorem LinearOrderedAddCommGroupWithTop.add_eq_top

added theorem LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_top

added theorem LinearOrderedAddCommGroupWithTop.neg_eq_top

added theorem LinearOrderedAddCommGroupWithTop.top_ne_zero