Theorem mul_le_of_nonneg_of_le_div

Modification history

2024-10-04 14:05
Mathlib/Algebra/Order/Field/Basic.lean
chore: generalise even more lemmas from `LinearOrderedField` to `GroupWithZero` (#17378)
Modified mul_le_of_nonneg_of_le_divView on Github →
2023-02-17 15:32
Mathlib/Algebra/Order/Field/Basic.lean
feat: `a ≤ b / c → a * c ≤ b` (#2027) …
Added mul_le_of_nonneg_of_le_divView on Github →