feat(GroupTheory/GroupAction/FixedPoints): characterise when there are no fixed points by an action (leanprover-community#38285)

Characterise when the set of points fixed by an action of a cancellative monoid action is empty.

Author: b-mehta

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_mul_eq_empty_iff [IsRightCancelMul M] {m : M} :
+    fixedBy M m = ∅ ↔ m ≠ 1 := by
+  simp [MulAction.fixedBy, Set.eq_empty_iff_forall_notMem]
+
+lemma fixedBy_mul_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