Theorem not_lt_one

Modification history

2026-05-06 19:54
Mathlib/Algebra/Order/IsBotOne.lean
feat: `IsBotOneClass` and `IsBotZeroClass` (#38730) …
Modified not_lt_oneView on Github →
2026-04-29 14:11
Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean
chore: make argument in `zero_le`/`one_le` implicit (#38148) …
Modified not_lt_oneView on Github →
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 →