Theorem Order.IsSuccLimit.ne_zero

Modification history

2026-05-10 00:45
Mathlib/Order/SuccPred/Limit.lean
feat(Algebra/Order/SuccPred): generalize `CanonicallyOrderedAdd` to `IsBotZeroClass` (#39062) …
Added Order.IsSuccLimit.ne_zeroView on Github →