fix

leanprover-community · Jan 26, 2024 · 5b8a432 · 5b8a432
1 parent 262bd1d
commit 5b8a432
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/Mathlib/GroupTheory/GroupAction/Basic.lean b/Mathlib/GroupTheory/GroupAction/Basic.lean
@@ -532,7 +532,6 @@ end AddAction
 attribute [to_additive existing] MulAction.stabilizer_smul_eq_stabilizer_map_conj
 attribute [to_additive existing] MulAction.stabilizerEquivStabilizerOfOrbitRel
 
-@[to_additive]
 theorem Equiv.swap_mem_stabilizer {α : Type*} [DecidableEq α] {S : Set α} {a b : α} :
     Equiv.swap a b ∈ MulAction.stabilizer (Equiv.Perm α) S ↔ (a ∈ S ↔ b ∈ S) := by
   rw [MulAction.mem_stabilizer_iff, Set.ext_iff, ← swap_inv]