From 09b44c176e0eaf2a3cbf11272dca8cbe8dfcda29 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Sat, 27 Jan 2024 19:32:54 +0000 Subject: [PATCH] feat(GroupTheory/GroupAction/Group): invOf smul lemmas (#9972) Give `smul` versions of some existing `mul` lemmas: - `invOf_smul_smul` - smul_invOf_smul (c.f. mul_invOf_self_assoc) - `invOf_smul_eq_iff` (c.f. `invOf_mul_eq_iff_eq_mul_left`) (required for #7569) - `smul_eq_iff_eq_invOf_smul` (c.f `mul_left_eq_iff_eq_invOf_mul`) Co-authored-by: Christopher Hoskin Co-authored-by: Christopher Hoskin --- Mathlib/GroupTheory/GroupAction/Group.lean | 23 ++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/Mathlib/GroupTheory/GroupAction/Group.lean b/Mathlib/GroupTheory/GroupAction/Group.lean index 66531b995e7e1..4b705f283db3f 100644 --- a/Mathlib/GroupTheory/GroupAction/Group.lean +++ b/Mathlib/GroupTheory/GroupAction/Group.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Hughes -/ import Mathlib.Algebra.Group.Aut +import Mathlib.Algebra.Invertible.Basic import Mathlib.GroupTheory.GroupAction.Units #align_import group_theory.group_action.group from "leanprover-community/mathlib"@"3b52265189f3fb43aa631edffce5d060fafaf82f" @@ -178,6 +179,28 @@ theorem smul_eq_iff_eq_inv_smul (g : α) {x y : β} : g • x = y ↔ x = g⁻¹ end Group +section Monoid + +variable [Monoid α] [MulAction α β] + +variable (c : α) (x y : β) [Invertible c] + +@[simp] +theorem invOf_smul_smul : ⅟c • c • x = x := inv_smul_smul (unitOfInvertible c) _ + +@[simp] +theorem smul_invOf_smul : c • (⅟ c • x) = x := smul_inv_smul (unitOfInvertible c) _ + +variable {c x y} + +theorem invOf_smul_eq_iff : ⅟c • x = y ↔ x = c • y := + inv_smul_eq_iff (a := unitOfInvertible c) + +theorem smul_eq_iff_eq_invOf_smul : c • x = y ↔ x = ⅟c • y := + smul_eq_iff_eq_inv_smul (g := unitOfInvertible c) + +end Monoid + /-- `Monoid.toMulAction` is faithful on nontrivial cancellative monoids with zero. -/ instance CancelMonoidWithZero.faithfulSMul [CancelMonoidWithZero α] [Nontrivial α] : FaithfulSMul α α :=