Theorem Left.one_lt_mul_of_left

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_leftView 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_leftView on Github →