From d82e37c7453a2bf9c24ea64fb559a2997024436a Mon Sep 17 00:00:00 2001 From: Geoffrey Irving Date: Thu, 15 Feb 2024 15:14:46 +0000 Subject: [PATCH 1/3] =?UTF-8?q?feat:=20`mul=5Finv=5Fle=5Fone=5Fof=5Fle`=20?= =?UTF-8?q?is=20an=20`a=20*=20b=E2=81=BB=C2=B9`=20`div=5Fle=5Fone=5Fof=5Fl?= =?UTF-8?q?e`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/Algebra/Order/Field/Basic.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Algebra/Order/Field/Basic.lean b/Mathlib/Algebra/Order/Field/Basic.lean index c3146893e8516..2e5500b81be28 100644 --- a/Mathlib/Algebra/Order/Field/Basic.lean +++ b/Mathlib/Algebra/Order/Field/Basic.lean @@ -243,6 +243,10 @@ 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 +/-- `a * b⁻¹` version of `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 + /-! ### Bi-implications of inequalities using inversions -/ From e567f883cdcc8576da489ff659ba7733e24db41d Mon Sep 17 00:00:00 2001 From: Geoffrey Irving Date: Thu, 15 Feb 2024 20:29:55 +0000 Subject: [PATCH 2/3] Add the symmetric inv_mul version --- Mathlib/Algebra/Order/Field/Basic.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Algebra/Order/Field/Basic.lean b/Mathlib/Algebra/Order/Field/Basic.lean index 2e5500b81be28..49a547a173b39 100644 --- a/Mathlib/Algebra/Order/Field/Basic.lean +++ b/Mathlib/Algebra/Order/Field/Basic.lean @@ -247,6 +247,10 @@ theorem div_le_one_of_le (h : a ≤ b) (hb : 0 ≤ b) : a / b ≤ 1 := 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 +/-- `b⁻¹ * a` version of `div_le_one_of_le` -/ +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 -/ From 563bd185286a45ff7a311a810f51f0f05362910f Mon Sep 17 00:00:00 2001 From: Geoffrey Irving Date: Tue, 20 Feb 2024 11:44:05 +0000 Subject: [PATCH 3/3] Remove bad docstrings MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Yaël Dillies --- Mathlib/Algebra/Order/Field/Basic.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Mathlib/Algebra/Order/Field/Basic.lean b/Mathlib/Algebra/Order/Field/Basic.lean index 49a547a173b39..dd25873c9e39a 100644 --- a/Mathlib/Algebra/Order/Field/Basic.lean +++ b/Mathlib/Algebra/Order/Field/Basic.lean @@ -243,11 +243,9 @@ 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 -/-- `a * b⁻¹` version of `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 -/-- `b⁻¹ * a` version of `div_le_one_of_le` -/ 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