Theorem Right.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 Right.one_lt_mul_of_left View on Github →

2026-04-05 08:48

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

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

Added Right.one_lt_mul_of_left View on Github →