feat: fix to_additive names in BigOperators.Basic (#1671)

Mathlib/Algebra/BigOperators/Basic.lean

@@ -1410,16 +1410,16 @@ theorem prod_const (b : β) : (∏ _x in s, b) = b ^ s.card :=
 #align finset.prod_const Finset.prod_const
 #align finset.sum_const Finset.sum_const
 
-@[to_additive]
+@[to_additive nsmul_eq_sum_const]
 theorem pow_eq_prod_const (b : β) : ∀ n, b ^ n = ∏ _k in range n, b := by simp
 #align finset.pow_eq_prod_const Finset.pow_eq_prod_const
-#align finset.smul_eq_sum_const Finset.smul_eq_sum_const
+#align finset.nsmul_eq_sum_const Finset.nsmul_eq_sum_const
 
-@[to_additive]
+@[to_additive sum_nsmul]
 theorem prod_pow (s : Finset α) (n : ℕ) (f : α → β) : (∏ x in s, f x ^ n) = (∏ x in s, f x) ^ n :=
   Multiset.prod_map_pow
 #align finset.prod_pow Finset.prod_pow
-#align finset.sum_smul Finset.sum_smul
+#align finset.sum_nsmul Finset.sum_nsmul
 
 @[to_additive]
 theorem prod_flip {n : ℕ} (f : ℕ → β) :
@@ -2105,7 +2105,7 @@ theorem exists_smul_of_dvd_count (s : Multiset α) {k : ℕ}
     apply Finset.sum_congr rfl
     intro x hx
     rw [← mul_nsmul', Nat.mul_div_cancel' (h x (mem_toFinset.mp hx))]
-  rw [← Finset.sum_smul, h₂, toFinset_sum_count_nsmul_eq]
+  rw [← Finset.sum_nsmul, h₂, toFinset_sum_count_nsmul_eq]
 #align multiset.exists_smul_of_dvd_count Multiset.exists_smul_of_dvd_count
 
 theorem toFinset_prod_dvd_prod [CommMonoid α] (S : Multiset α) : S.toFinset.prod id ∣ S.prod := by