From 3894e48954a10152ecbb659757c5ecd3585cee12 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sat, 29 Apr 2023 16:26:38 +0000 Subject: [PATCH] =?UTF-8?q?feat:=20`a=20*=20b=20=E2=89=A0=20b=20=E2=86=94?= =?UTF-8?q?=20a=20=E2=89=A0=201`=20(#3726)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit https://github.com/leanprover-community/mathlib/pull/18635 * [`algebra.group.basic`@`2196ab363eb097c008d4497125e0dde23fb36db2`..`84771a9f5f0bd5e5d6218811556508ddf476dcbd`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/basic?range=2196ab363eb097c008d4497125e0dde23fb36db2..84771a9f5f0bd5e5d6218811556508ddf476dcbd) * [`algebra.order.field.basic`@`44e29dbcff83ba7114a464d592b8c3743987c1e5`..`84771a9f5f0bd5e5d6218811556508ddf476dcbd`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/field/basic?range=44e29dbcff83ba7114a464d592b8c3743987c1e5..84771a9f5f0bd5e5d6218811556508ddf476dcbd) Co-authored-by: Eric Wieser --- Mathlib/Algebra/Group/Basic.lean | 22 ++++++++++++++++++- Mathlib/Algebra/Order/Field/Basic.lean | 29 ++++++++++++++------------ 2 files changed, 37 insertions(+), 14 deletions(-) diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean index 46f3a82f18d66..4291b7c65cf09 100644 --- a/Mathlib/Algebra/Group/Basic.lean +++ b/Mathlib/Algebra/Group/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro ! This file was ported from Lean 3 source module algebra.group.basic -! leanprover-community/mathlib commit 2196ab363eb097c008d4497125e0dde23fb36db2 +! leanprover-community/mathlib commit 84771a9f5f0bd5e5d6218811556508ddf476dcbd ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -191,6 +191,16 @@ theorem self_eq_mul_right : a = a * b ↔ b = 1 := #align self_eq_mul_right self_eq_mul_right #align self_eq_add_right self_eq_add_right +@[to_additive] +theorem mul_right_ne_self : a * b ≠ a ↔ b ≠ 1 := mul_right_eq_self.not +#align mul_right_ne_self mul_right_ne_self +#align add_right_ne_self add_right_ne_self + +@[to_additive] +theorem self_ne_mul_right : a ≠ a * b ↔ b ≠ 1 := self_eq_mul_right.not +#align self_ne_mul_right self_ne_mul_right +#align self_ne_add_right self_ne_add_right + end LeftCancelMonoid section RightCancelMonoid @@ -210,6 +220,16 @@ theorem self_eq_mul_left : b = a * b ↔ a = 1 := #align self_eq_mul_left self_eq_mul_left #align self_eq_add_left self_eq_add_left +@[to_additive] +theorem mul_left_ne_self : a * b ≠ b ↔ a ≠ 1 := mul_left_eq_self.not +#align mul_left_ne_self mul_left_ne_self +#align add_left_ne_self add_left_ne_self + +@[to_additive] +theorem self_ne_mul_left : b ≠ a * b ↔ a ≠ 1 := self_eq_mul_left.not +#align self_ne_mul_left self_ne_mul_left +#align self_ne_add_left self_ne_add_left + end RightCancelMonoid section InvolutiveInv diff --git a/Mathlib/Algebra/Order/Field/Basic.lean b/Mathlib/Algebra/Order/Field/Basic.lean index fbc24125a3bf4..e7bacad44b7f2 100644 --- a/Mathlib/Algebra/Order/Field/Basic.lean +++ b/Mathlib/Algebra/Order/Field/Basic.lean @@ -3,7 +3,7 @@ Copyright (c) 2014 Robert Lewis. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Robert Lewis, Leonardo de Moura, Mario Carneiro, Floris van Doorn ! This file was ported from Lean 3 source module algebra.order.field.basic -! leanprover-community/mathlib commit 44e29dbcff83ba7114a464d592b8c3743987c1e5 +! leanprover-community/mathlib commit 84771a9f5f0bd5e5d6218811556508ddf476dcbd ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -511,22 +511,25 @@ theorem one_half_pos : (0 : α) < 1 / 2 := half_pos zero_lt_one #align one_half_pos one_half_pos -theorem div_two_lt_of_pos (h : 0 < a) : a / 2 < a := by - rw [div_lt_iff (zero_lt_two' α)] - exact lt_mul_of_one_lt_right h one_lt_two -#align div_two_lt_of_pos div_two_lt_of_pos +@[simp] +theorem half_le_self_iff : a / 2 ≤ a ↔ 0 ≤ a := by + rw [div_le_iff (zero_lt_two' α), mul_two, le_add_iff_nonneg_left] +#align half_le_self_iff half_le_self_iff -theorem half_lt_self : 0 < a → a / 2 < a := - div_two_lt_of_pos -#align half_lt_self half_lt_self +@[simp] +theorem half_lt_self_iff : a / 2 < a ↔ 0 < a := by + rw [div_lt_iff (zero_lt_two' α), mul_two, lt_add_iff_pos_left] +#align half_lt_self_iff half_lt_self_iff -theorem half_le_self (ha_nonneg : 0 ≤ a) : a / 2 ≤ a := by - by_cases h0 : a = 0 - · simp [h0] - · rw [← Ne.def] at h0 - exact (half_lt_self (lt_of_le_of_ne ha_nonneg h0.symm)).le +alias half_le_self_iff ↔ _ half_le_self #align half_le_self half_le_self +alias half_lt_self_iff ↔ _ half_lt_self +#align half_lt_self half_lt_self + +alias half_lt_self ← div_two_lt_of_pos +#align div_two_lt_of_pos div_two_lt_of_pos + theorem one_half_lt_one : (1 / 2 : α) < 1 := half_lt_self zero_lt_one #align one_half_lt_one one_half_lt_one