Theorem LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_top

Modification history

2025-12-17 18:54
Mathlib/Algebra/Order/AddGroupWithTop.lean
chore(Algebra/Order/AddGroupWithTop): golf (#32382)
Deleted LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_topView on Github →
2024-11-06 04:34
Mathlib/Algebra/Order/AddGroupWithTop.lean
feat: SubtractionMonoid instance for LinearOrderedAddCommGroupWithTop (#18665)
Added LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_topView on Github →