Theorem mul_div_mul_right_le

Modification history

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