Theorem one_lt_of_gt

Modification history

2026-05-06 19:54

Mathlib/Algebra/Order/IsBotOne.lean

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

Modified one_lt_of_gt View on Github →

2025-01-16 10:00

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

refactor: make `CanonicallyOrdered...` mixin (#17444) …

Added one_lt_of_gt View on Github →