Theorem isBot_one

Modification history

2026-05-06 19:54

Mathlib/Algebra/Order/IsBotOne.lean

feat: `IsBotOneClass` and `IsBotZeroClass` (#38730) …

Modified isBot_one View 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 isBot_one View on Github →

2025-05-13 08:28

Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

chore: remove `CanonicallyOrdered{Mul, Add}.toOrderBot` (#24094) …

Added isBot_one View on Github →