Theorem one_le

Modification history

2026-05-06 19:54

Mathlib/Algebra/Order/IsBotOne.lean

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

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

2022-12-01 10:59

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

feat: port Algebra.Order.Monoid.Canonical.Defs (#778) …

Added one_le View on Github →