Commit 2023-03-29 06:53 1e9f59dd

View on Github →

chore: forward port leanprover-community/mathlib#18667 (#3163)

Estimated changes

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

added theorem le_mul_of_le_left

added theorem le_mul_of_le_right

Modified Mathlib/Algebra/Order/Monoid/MinMax.lean

added theorem le_or_le_of_mul_le_mul

added theorem le_or_lt_of_mul_le_mul

added theorem lt_or_le_of_mul_le_mul

modified theorem lt_or_lt_of_mul_lt_mul

modified theorem mul_lt_mul_iff_of_le_of_le

Modified Mathlib/Order/Basic.lean

added theorem gt_or_eq_of_le