Theorem ne_one_of_lt

Modification history

2026-05-06 19:54

Mathlib/Algebra/Order/IsBotOne.lean

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

Modified ne_one_of_lt 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) …

Added ne_one_of_lt View on Github →