Theorem Left.one_lt_mul_of_right

Modification history

2026-05-06 19:54

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

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

Modified Left.one_lt_mul_of_right View on Github →

2026-04-05 08:48

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

feat: `0 < a` → `0 < a + b` (#37641)

Added Left.one_lt_mul_of_right View on Github →