Theorem Right.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 Right.one_lt_mul_of_rightView 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_rightView on Github →