Theorem not_lt_one

Modification history

2025-12-04 16:59
Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean
chore(Algebra/Order): deprecate `not_neg` in favour of `not_lt_zero` (#32397) …
Modified not_lt_oneView on Github →
2025-11-24 14:11
Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean
feat: no element is strictly negative in a canonically ordered monoid (#31894) …
Added not_lt_oneView on Github →