Theorem IsAddRegular.of_ne_top

Modification history

2026-01-08 11:26
Mathlib/Algebra/Order/AddGroupWithTop.lean
refactor: make `LinearOrderedCommMonoidWithZero`s cancellative (#31749) …
Added IsAddRegular.of_ne_topView on Github →