From d0542a8b4e3b696815c4274b2327ca72062a2e7f Mon Sep 17 00:00:00 2001 From: Geoffrey Irving Date: Thu, 22 Feb 2024 09:41:17 +0000 Subject: [PATCH] feat: Add `mul_inv` and `inv_mul` versions of `div_le_one_of_le` (#10597) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit These are exactly `div_le_one_of_le` with `a / b` replaced by `a * b⁻¹` and `b⁻¹ * a`. They come up frequently because some tactics produce inverses as normal forms over division. The iff versions with `0 < b` already exist as `mul_inv_le_one_iff` and `inv_mul_le_one_iff`; the point of these is to have a weaker nonnegativity assumption on `b`. --- Mathlib/Algebra/Order/Field/Basic.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Mathlib/Algebra/Order/Field/Basic.lean b/Mathlib/Algebra/Order/Field/Basic.lean index c3146893e85168..dd25873c9e39aa 100644 --- a/Mathlib/Algebra/Order/Field/Basic.lean +++ b/Mathlib/Algebra/Order/Field/Basic.lean @@ -243,6 +243,12 @@ theorem div_le_one_of_le (h : a ≤ b) (hb : 0 ≤ b) : a / b ≤ 1 := div_le_of_nonneg_of_le_mul hb zero_le_one <| by rwa [one_mul] #align div_le_one_of_le div_le_one_of_le +lemma mul_inv_le_one_of_le (h : a ≤ b) (hb : 0 ≤ b) : a * b⁻¹ ≤ 1 := by + simpa only [← div_eq_mul_inv] using div_le_one_of_le h hb + +lemma inv_mul_le_one_of_le (h : a ≤ b) (hb : 0 ≤ b) : b⁻¹ * a ≤ 1 := by + simpa only [← div_eq_inv_mul] using div_le_one_of_le h hb + /-! ### Bi-implications of inequalities using inversions -/