From c8d50df101dfbcab82880b4850ce4ece7922d83a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 5 Jan 2024 11:32:31 +0000 Subject: [PATCH] chore: Move `Commute` results earlier (#9440) These lemmas aren't really proved any faster using units, and I will soon need them not to be proved using units. Part of #9411 --- Mathlib/Algebra/Group/Commute/Basic.lean | 34 +++++++++++++ Mathlib/Algebra/Group/Commute/Units.lean | 61 ----------------------- Mathlib/Algebra/Group/Defs.lean | 14 ++++++ Mathlib/Algebra/Group/Semiconj/Basic.lean | 36 +++++++++---- Mathlib/Algebra/Group/Semiconj/Units.lean | 32 ------------ Mathlib/Algebra/GroupPower/Basic.lean | 4 +- Mathlib/Data/Int/Basic.lean | 5 -- 7 files changed, 77 insertions(+), 109 deletions(-) diff --git a/Mathlib/Algebra/Group/Commute/Basic.lean b/Mathlib/Algebra/Group/Commute/Basic.lean index 52526a31626af..ec86249c341d1 100644 --- a/Mathlib/Algebra/Group/Commute/Basic.lean +++ b/Mathlib/Algebra/Group/Commute/Basic.lean @@ -58,4 +58,38 @@ protected theorem div_div_div_comm (hbc : Commute b c) (hbd : Commute b⁻¹ d) end DivisionMonoid +section Group +variable [Group G] {a b : G} + +@[to_additive (attr := simp)] +lemma inv_left_iff : Commute a⁻¹ b ↔ Commute a b := SemiconjBy.inv_symm_left_iff +#align commute.inv_left_iff Commute.inv_left_iff +#align add_commute.neg_left_iff AddCommute.neg_left_iff + +@[to_additive] alias ⟨_, inv_left⟩ := inv_left_iff +#align commute.inv_left Commute.inv_left +#align add_commute.neg_left AddCommute.neg_left + +@[to_additive (attr := simp)] +lemma inv_right_iff : Commute a b⁻¹ ↔ Commute a b := SemiconjBy.inv_right_iff +#align commute.inv_right_iff Commute.inv_right_iff +#align add_commute.neg_right_iff AddCommute.neg_right_iff + +@[to_additive] alias ⟨_, inv_right⟩ := inv_right_iff +#align commute.inv_right Commute.inv_right +#align add_commute.neg_right AddCommute.neg_right + +@[to_additive] +protected lemma inv_mul_cancel (h : Commute a b) : a⁻¹ * b * a = b := by + rw [h.inv_left.eq, inv_mul_cancel_right] +#align commute.inv_mul_cancel Commute.inv_mul_cancel +#align add_commute.neg_add_cancel AddCommute.neg_add_cancel + +@[to_additive] +lemma inv_mul_cancel_assoc (h : Commute a b) : a⁻¹ * (b * a) = b := by + rw [← mul_assoc, h.inv_mul_cancel] +#align commute.inv_mul_cancel_assoc Commute.inv_mul_cancel_assoc +#align add_commute.neg_add_cancel_assoc AddCommute.neg_add_cancel_assoc + +end Group end Commute diff --git a/Mathlib/Algebra/Group/Commute/Units.lean b/Mathlib/Algebra/Group/Commute/Units.lean index ab88e7de6d631..e047ec8da22da 100644 --- a/Mathlib/Algebra/Group/Commute/Units.lean +++ b/Mathlib/Algebra/Group/Commute/Units.lean @@ -99,65 +99,4 @@ theorem _root_.isUnit_mul_self_iff : IsUnit (a * a) ↔ IsUnit a := #align is_add_unit_add_self_iff isAddUnit_add_self_iff end Monoid - -section Group - -variable [Group G] {a b : G} - -@[to_additive] -theorem inv_right : Commute a b → Commute a b⁻¹ := - SemiconjBy.inv_right -#align commute.inv_right Commute.inv_right -#align add_commute.neg_right AddCommute.neg_right - -@[to_additive (attr := simp)] -theorem inv_right_iff : Commute a b⁻¹ ↔ Commute a b := - SemiconjBy.inv_right_iff -#align commute.inv_right_iff Commute.inv_right_iff -#align add_commute.neg_right_iff AddCommute.neg_right_iff - -@[to_additive] -theorem inv_left : Commute a b → Commute a⁻¹ b := - SemiconjBy.inv_symm_left -#align commute.inv_left Commute.inv_left -#align add_commute.neg_left AddCommute.neg_left - -@[to_additive (attr := simp)] -theorem inv_left_iff : Commute a⁻¹ b ↔ Commute a b := - SemiconjBy.inv_symm_left_iff -#align commute.inv_left_iff Commute.inv_left_iff -#align add_commute.neg_left_iff AddCommute.neg_left_iff - -@[to_additive] -protected theorem inv_mul_cancel (h : Commute a b) : a⁻¹ * b * a = b := by - rw [h.inv_left.eq, inv_mul_cancel_right] -#align commute.inv_mul_cancel Commute.inv_mul_cancel -#align add_commute.neg_add_cancel AddCommute.neg_add_cancel - -@[to_additive] -theorem inv_mul_cancel_assoc (h : Commute a b) : a⁻¹ * (b * a) = b := by - rw [← mul_assoc, h.inv_mul_cancel] -#align commute.inv_mul_cancel_assoc Commute.inv_mul_cancel_assoc -#align add_commute.neg_add_cancel_assoc AddCommute.neg_add_cancel_assoc - -end Group - end Commute - -section CommGroup - -variable [CommGroup G] (a b : G) - -@[to_additive (attr := simp)] -theorem inv_mul_cancel_comm : a⁻¹ * b * a = b := - (Commute.all a b).inv_mul_cancel -#align inv_mul_cancel_comm inv_mul_cancel_comm -#align neg_add_cancel_comm neg_add_cancel_comm - -@[to_additive (attr := simp)] -theorem inv_mul_cancel_comm_assoc : a⁻¹ * (b * a) = b := - (Commute.all a b).inv_mul_cancel_assoc -#align inv_mul_cancel_comm_assoc inv_mul_cancel_comm_assoc -#align neg_add_cancel_comm_assoc neg_add_cancel_comm_assoc - -end CommGroup diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean index 96578316890a6..5871222cc782d 100644 --- a/Mathlib/Algebra/Group/Defs.lean +++ b/Mathlib/Algebra/Group/Defs.lean @@ -998,6 +998,10 @@ theorem zpow_ofNat (a : G) : ∀ n : ℕ, a ^ (n : ℤ) = a ^ n #align zpow_of_nat zpow_ofNat #align of_nat_zsmul ofNat_zsmul +@[to_additive (attr := simp, norm_cast) coe_nat_zsmul] +lemma zpow_coe_nat (a : G) (n : ℕ) : a ^ (Nat.cast n : ℤ) = a ^ n := zpow_ofNat .. +#align coe_nat_zsmul coe_nat_zsmul + theorem zpow_negSucc (a : G) (n : ℕ) : a ^ (Int.negSucc n) = (a ^ (n + 1))⁻¹ := by rw [← zpow_ofNat] exact DivInvMonoid.zpow_neg' n a @@ -1263,6 +1267,16 @@ instance (priority := 100) CommGroup.toCancelCommMonoid : CancelCommMonoid G := instance (priority := 100) CommGroup.toDivisionCommMonoid : DivisionCommMonoid G := { ‹CommGroup G›, Group.toDivisionMonoid with } +@[to_additive (attr := simp)] lemma inv_mul_cancel_comm (a b : G) : a⁻¹ * b * a = b := by + rw [mul_comm, mul_inv_cancel_left] +#align inv_mul_cancel_comm inv_mul_cancel_comm +#align neg_add_cancel_comm neg_add_cancel_comm + +@[to_additive (attr := simp)] lemma inv_mul_cancel_comm_assoc (a b : G) : a⁻¹ * (b * a) = b := by + rw [mul_comm, mul_inv_cancel_right] +#align inv_mul_cancel_comm_assoc inv_mul_cancel_comm_assoc +#align neg_add_cancel_comm_assoc neg_add_cancel_comm_assoc + end CommGroup /-! We initialize all projections for `@[simps]` here, so that we don't have to do it in later diff --git a/Mathlib/Algebra/Group/Semiconj/Basic.lean b/Mathlib/Algebra/Group/Semiconj/Basic.lean index 05a807fabfd96..b3ff872fd9cf9 100644 --- a/Mathlib/Algebra/Group/Semiconj/Basic.lean +++ b/Mathlib/Algebra/Group/Semiconj/Basic.lean @@ -9,29 +9,47 @@ import Mathlib.Algebra.Group.Basic #align_import algebra.group.semiconj from "leanprover-community/mathlib"@"a148d797a1094ab554ad4183a4ad6f130358ef64" /-! -# Lemmas about semiconjugate elements of a semigroup +# Lemmas about semiconjugate elements of a group -/ namespace SemiconjBy +variable {G : Type*} section DivisionMonoid - -variable {G : Type*} [DivisionMonoid G] {a x y : G} +variable [DivisionMonoid G] {a x y : G} @[to_additive (attr := simp)] -theorem inv_inv_symm_iff : SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x := - inv_involutive.injective.eq_iff.symm.trans <| by - rw [mul_inv_rev, mul_inv_rev, inv_inv, inv_inv, inv_inv, eq_comm, SemiconjBy] +theorem inv_inv_symm_iff : SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x := by + simp_rw [SemiconjBy, ← mul_inv_rev, inv_inj, eq_comm] #align semiconj_by.inv_inv_symm_iff SemiconjBy.inv_inv_symm_iff #align add_semiconj_by.neg_neg_symm_iff AddSemiconjBy.neg_neg_symm_iff -@[to_additive] -theorem inv_inv_symm : SemiconjBy a x y → SemiconjBy a⁻¹ y⁻¹ x⁻¹ := - inv_inv_symm_iff.2 +@[to_additive] alias ⟨_, inv_inv_symm⟩ := inv_inv_symm_iff #align semiconj_by.inv_inv_symm SemiconjBy.inv_inv_symm #align add_semiconj_by.neg_neg_symm AddSemiconjBy.neg_neg_symm end DivisionMonoid +section Group +variable [Group G] {a x y : G} + +@[to_additive (attr := simp)] lemma inv_symm_left_iff : SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y := by + simp_rw [SemiconjBy, eq_mul_inv_iff_mul_eq, mul_assoc, inv_mul_eq_iff_eq_mul, eq_comm] +#align semiconj_by.inv_symm_left_iff SemiconjBy.inv_symm_left_iff +#align add_semiconj_by.neg_symm_left_iff AddSemiconjBy.neg_symm_left_iff + +@[to_additive] alias ⟨_, inv_symm_left⟩ := inv_symm_left_iff +#align semiconj_by.inv_symm_left SemiconjBy.inv_symm_left +#align add_semiconj_by.neg_symm_left AddSemiconjBy.neg_symm_left + +@[to_additive (attr := simp)] lemma inv_right_iff : SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y := by + rw [← inv_symm_left_iff, inv_inv_symm_iff] +#align add_semiconj_by.neg_right_iff AddSemiconjBy.neg_right_iff + +@[to_additive] alias ⟨_, inv_right⟩ := inv_right_iff +#align semiconj_by.inv_right SemiconjBy.inv_right +#align add_semiconj_by.neg_right AddSemiconjBy.neg_right + +end Group end SemiconjBy diff --git a/Mathlib/Algebra/Group/Semiconj/Units.lean b/Mathlib/Algebra/Group/Semiconj/Units.lean index 065963366ee40..b2a42301446fa 100644 --- a/Mathlib/Algebra/Group/Semiconj/Units.lean +++ b/Mathlib/Algebra/Group/Semiconj/Units.lean @@ -88,38 +88,6 @@ theorem units_val_iff {a x y : Mˣ} : SemiconjBy (a : M) x y ↔ SemiconjBy a x #align add_semiconj_by.add_units_coe_iff AddSemiconjBy.addUnits_val_iff end Monoid - -section Group - -variable [Group G] {a x y : G} - -@[to_additive (attr := simp)] -theorem inv_right_iff : SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y := - @units_inv_right_iff G _ a ⟨x, x⁻¹, mul_inv_self x, inv_mul_self x⟩ - ⟨y, y⁻¹, mul_inv_self y, inv_mul_self y⟩ -#align semiconj_by.inv_right_iff SemiconjBy.inv_right_iff -#align add_semiconj_by.neg_right_iff AddSemiconjBy.neg_right_iff - -@[to_additive] -theorem inv_right : SemiconjBy a x y → SemiconjBy a x⁻¹ y⁻¹ := - inv_right_iff.2 -#align semiconj_by.inv_right SemiconjBy.inv_right -#align add_semiconj_by.neg_right AddSemiconjBy.neg_right - -@[to_additive (attr := simp)] -theorem inv_symm_left_iff : SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y := - @units_inv_symm_left_iff G _ ⟨a, a⁻¹, mul_inv_self a, inv_mul_self a⟩ _ _ -#align semiconj_by.inv_symm_left_iff SemiconjBy.inv_symm_left_iff -#align add_semiconj_by.neg_symm_left_iff AddSemiconjBy.neg_symm_left_iff - -@[to_additive] -theorem inv_symm_left : SemiconjBy a x y → SemiconjBy a⁻¹ y x := - inv_symm_left_iff.2 -#align semiconj_by.inv_symm_left SemiconjBy.inv_symm_left -#align add_semiconj_by.neg_symm_left AddSemiconjBy.neg_symm_left - -end Group - end SemiconjBy /-- `a` semiconjugates `x` to `a * x * a⁻¹`. -/ diff --git a/Mathlib/Algebra/GroupPower/Basic.lean b/Mathlib/Algebra/GroupPower/Basic.lean index 7987521fafe72..71c1aff51bd68 100644 --- a/Mathlib/Algebra/GroupPower/Basic.lean +++ b/Mathlib/Algebra/GroupPower/Basic.lean @@ -3,9 +3,9 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Robert Y. Lewis -/ -import Mathlib.Algebra.Group.Commute.Units +import Mathlib.Algebra.Group.Commute.Basic import Mathlib.Algebra.GroupWithZero.Defs -import Mathlib.Tactic.Convert +import Mathlib.Tactic.Common #align_import algebra.group_power.basic from "leanprover-community/mathlib"@"9b2660e1b25419042c8da10bf411aa3c67f14383" diff --git a/Mathlib/Data/Int/Basic.lean b/Mathlib/Data/Int/Basic.lean index be0dd2169bc10..d608336210a56 100644 --- a/Mathlib/Data/Int/Basic.lean +++ b/Mathlib/Data/Int/Basic.lean @@ -88,11 +88,6 @@ lemma natAbs_cast (n : ℕ) : natAbs ↑n = n := rfl @[norm_cast] protected lemma coe_nat_sub {n m : ℕ} : n ≤ m → (↑(m - n) : ℤ) = ↑m - ↑n := ofNat_sub -@[to_additive (attr := simp, norm_cast) coe_nat_zsmul] -theorem _root_.zpow_coe_nat [DivInvMonoid G] (a : G) (n : ℕ) : a ^ (Nat.cast n : ℤ) = a ^ n := - zpow_ofNat .. -#align coe_nat_zsmul coe_nat_zsmul - /-! ### Extra instances to short-circuit type class resolution These also prevent non-computable instances like `Int.normedCommRing` being used to construct