Theorem WithTop.LinearOrderedAddCommGroup.sub_eq_top_iff

Modification history

2025-12-17 18:54
Mathlib/Algebra/Order/AddGroupWithTop.lean
chore(Algebra/Order/AddGroupWithTop): golf (#32382)
Modified WithTop.LinearOrderedAddCommGroup.sub_eq_top_iffView on Github →
2024-07-12 07:41
Mathlib/Algebra/Order/AddGroupWithTop.lean
chore: move non `@[to_additive]` parts of `Algebra.Order.Monoid` and `Algebra.Order.Group` to a different file (#14667) …
Modified WithTop.LinearOrderedAddCommGroup.sub_eq_top_iffView on Github →
2024-06-11 07:52
Mathlib/Algebra/Order/Group/WithTop.lean
chore: fix diamond for WithTop subtraction (#13715) …
Added WithTop.LinearOrderedAddCommGroup.sub_eq_top_iffView on Github →