Theorem le_mul_div_mul_right

Modification history

2025-04-26 03:37
Mathlib/Algebra/Order/Field/Defs.lean
feat(Algebra/Order/Field/Defs): generalize lemmas (#24377) …
Modified le_mul_div_mul_rightView on Github →
2024-10-07 22:13
Mathlib/Algebra/Order/Field/Defs.lean
feat: `c * a / (c * b) ≤ a / b` (#17506)
Added le_mul_div_mul_rightView on Github →