From b3ea7c7a827b14ada93fe63137a5c705a0e7efab Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Mon, 20 Apr 2026 09:58:00 +0000 Subject: [PATCH] feat(GroupTheory/GroupAction/FixedPoints): add fixedBy_eq_empty_iff --- Mathlib/GroupTheory/GroupAction/FixedPoints.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Mathlib/GroupTheory/GroupAction/FixedPoints.lean b/Mathlib/GroupTheory/GroupAction/FixedPoints.lean index ecb6e5dfad05f4..677de49753729e 100644 --- a/Mathlib/GroupTheory/GroupAction/FixedPoints.lean +++ b/Mathlib/GroupTheory/GroupAction/FixedPoints.lean @@ -119,6 +119,14 @@ theorem smul_fixedBy (g h : G) : ext a simp_rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, mul_smul, smul_eq_iff_eq_inv_smul h] +lemma fixedBy_eq_empty_iff [IsRightCancelMul M] {m : M} : + fixedBy M m = ∅ ↔ m ≠ 1 := by + simp [MulAction.fixedBy, Set.eq_empty_iff_forall_notMem] + +lemma fixedBy_op_eq_empty_iff [IsLeftCancelMul M] {m : M} : + fixedBy M (MulOpposite.op m) = ∅ ↔ m ≠ 1 := by + simp [MulAction.fixedBy, Set.eq_empty_iff_forall_notMem] + end FixedPoints section Pointwise