diff --git a/Mathlib/Data/Set/Pointwise/ListOfFn.lean b/Mathlib/Data/Set/Pointwise/ListOfFn.lean
index c93b3c4f1bfd0..ccfc0dec6ee1e 100644
--- a/Mathlib/Data/Set/Pointwise/ListOfFn.lean
+++ b/Mathlib/Data/Set/Pointwise/ListOfFn.lean
@@ -55,10 +55,11 @@ theorem mem_list_prod {l : List (Set α)} {a : α} :
 #align set.mem_list_prod Set.mem_list_prod
 #align set.mem_list_sum Set.mem_list_sum
 
-@[to_additive mem_mul]
+@[to_additive]
 theorem mem_pow {a : α} {n : ℕ} :
     a ∈ s ^ n ↔ ∃ f : Fin n → s, (List.ofFn fun i ↦ (f i : α)).prod = a := by
   rw [← mem_prod_list_ofFn, List.ofFn_const, List.prod_replicate]
 #align set.mem_pow Set.mem_pow
+#align set.mem_nsmul Set.mem_nsmul
 
 end Set