From f66ae52a871c3a070352957a99eb54238bb8e060 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 11 May 2023 13:33:34 +0000 Subject: [PATCH 1/2] =?UTF-8?q?refactor:=20Redefine=20`a=20=E2=89=A1=20b?= =?UTF-8?q?=20[PMOD=20p]`=20Match=20https://github.com/leanprover-communit?= =?UTF-8?q?y/mathlib/pull/18958?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * [`algebra.group.basic`@`84771a9f5f0bd5e5d6218811556508ddf476dcbd`..`a07d750983b94c530ab69a726862c2ab6802b38c`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/basic?range=84771a9f5f0bd5e5d6218811556508ddf476dcbd..a07d750983b94c530ab69a726862c2ab6802b38c) * [`algebra.group_power.lemmas`@`e655e4ea5c6d02854696f97494997ba4c31be802`..`a07d750983b94c530ab69a726862c2ab6802b38c`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group_power/lemmas?range=e655e4ea5c6d02854696f97494997ba4c31be802..a07d750983b94c530ab69a726862c2ab6802b38c) * [`algebra.hom.units`@`dc6c365e751e34d100e80fe6e314c3c3e0fd2988`..`a07d750983b94c530ab69a726862c2ab6802b38c`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/hom/units?range=dc6c365e751e34d100e80fe6e314c3c3e0fd2988..a07d750983b94c530ab69a726862c2ab6802b38c) --- Mathlib/Algebra/Group/Basic.lean | 7 ++++++- Mathlib/Algebra/GroupPower/Lemmas.lean | 9 ++++++++- Mathlib/Algebra/Hom/Units.lean | 5 +++-- 3 files changed, 17 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean index 4291b7c65cf09..b31f981b438e9 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 84771a9f5f0bd5e5d6218811556508ddf476dcbd +! leanprover-community/mathlib commit a07d750983b94c530ab69a726862c2ab6802b38c ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -755,6 +755,11 @@ theorem mul_div_cancel'' (a b : G) : a * b / b = a := #align mul_div_cancel'' mul_div_cancel'' #align add_sub_cancel add_sub_cancel +@[to_additive (attr := simp) sub_add_cancel''] +theorem div_mul_cancel''' (a b : G) : a / (b * a) = b⁻¹ := by rw [← inv_div, mul_div_cancel''] +#align div_mul_cancel''' div_mul_cancel''' +#align sub_add_cancel'' sub_add_cancel'' + @[to_additive (attr := simp)] theorem mul_div_mul_right_eq_div (a b c : G) : a * c / (b * c) = a / b := by rw [div_mul_eq_div_div_swap]; simp only [mul_left_inj, eq_self_iff_true, mul_div_cancel''] diff --git a/Mathlib/Algebra/GroupPower/Lemmas.lean b/Mathlib/Algebra/GroupPower/Lemmas.lean index aaee94904dd54..b5bfc7c9e8537 100644 --- a/Mathlib/Algebra/GroupPower/Lemmas.lean +++ b/Mathlib/Algebra/GroupPower/Lemmas.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Robert Y. Lewis ! This file was ported from Lean 3 source module algebra.group_power.lemmas -! leanprover-community/mathlib commit e655e4ea5c6d02854696f97494997ba4c31be802 +! leanprover-community/mathlib commit a07d750983b94c530ab69a726862c2ab6802b38c ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -579,6 +579,13 @@ theorem mul_bit1 [NonAssocRing R] {n r : R} : r * bit1 n = (2 : ℤ) • (r * n) end bit0_bit1 +/-- Note this holds in marginally more generality than `Int.cast_mul` -/ +theorem Int.cast_mul_eq_zsmul_cast [AddCommGroupWithOne α] : ∀ m n, ((m * n : ℤ) : α) = m • n := + fun m => + Int.inductionOn' m 0 (by simp) (fun k _ ih n => by simp [add_mul, add_zsmul, ih]) fun k _ ih n => + by simp [sub_mul, sub_zsmul, ih, ← sub_eq_add_neg] +#align int.cast_mul_eq_zsmul_cast Int.cast_mul_eq_zsmul_cast + @[simp] theorem zsmul_eq_mul [Ring R] (a : R) : ∀ n : ℤ, n • a = n * a | (n : ℕ) => by rw [coe_nat_zsmul, nsmul_eq_mul, Int.cast_ofNat] diff --git a/Mathlib/Algebra/Hom/Units.lean b/Mathlib/Algebra/Hom/Units.lean index 7b3929b9ee1b2..47d6759ba3ea6 100644 --- a/Mathlib/Algebra/Hom/Units.lean +++ b/Mathlib/Algebra/Hom/Units.lean @@ -5,7 +5,7 @@ Authors: Johan Commelin, Chris Hughes, Kevin Buzzard Ported by: Winston Yin ! This file was ported from Lean 3 source module algebra.hom.units -! leanprover-community/mathlib commit dc6c365e751e34d100e80fe6e314c3c3e0fd2988 +! leanprover-community/mathlib commit a07d750983b94c530ab69a726862c2ab6802b38c ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -437,7 +437,8 @@ protected theorem div_eq_one_iff_eq (h : IsUnit b) : a / b = 1 ↔ a = b := #align is_unit.div_eq_one_iff_eq IsUnit.div_eq_one_iff_eq #align is_add_unit.sub_eq_zero_iff_eq IsAddUnit.sub_eq_zero_iff_eq -@[to_additive] +/-- The `group` version of this lemma is `div_mul_cancel'''` -/ +@[to_additive "The `add_group` version of this lemma is `sub_add_cancel''`"] protected theorem div_mul_left (h : IsUnit b) : b / (a * b) = 1 / a := by rw [div_eq_mul_inv, mul_inv_rev, h.mul_inv_cancel_left, one_div] #align is_unit.div_mul_left IsUnit.div_mul_left From 4cc2ea16473f0c73bb3d570161d0991b32b2d809 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 11 May 2023 18:48:05 +0100 Subject: [PATCH 2/2] Update Mathlib/Algebra/Hom/Units.lean --- Mathlib/Algebra/Hom/Units.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Hom/Units.lean b/Mathlib/Algebra/Hom/Units.lean index 47d6759ba3ea6..f861563634838 100644 --- a/Mathlib/Algebra/Hom/Units.lean +++ b/Mathlib/Algebra/Hom/Units.lean @@ -437,8 +437,8 @@ protected theorem div_eq_one_iff_eq (h : IsUnit b) : a / b = 1 ↔ a = b := #align is_unit.div_eq_one_iff_eq IsUnit.div_eq_one_iff_eq #align is_add_unit.sub_eq_zero_iff_eq IsAddUnit.sub_eq_zero_iff_eq -/-- The `group` version of this lemma is `div_mul_cancel'''` -/ -@[to_additive "The `add_group` version of this lemma is `sub_add_cancel''`"] +/-- The `Group` version of this lemma is `div_mul_cancel'''` -/ +@[to_additive "The `AddGroup` version of this lemma is `sub_add_cancel''`"] protected theorem div_mul_left (h : IsUnit b) : b / (a * b) = 1 / a := by rw [div_eq_mul_inv, mul_inv_rev, h.mul_inv_cancel_left, one_div] #align is_unit.div_mul_left IsUnit.div_mul_left