refactor(data/multiset/basic): consistently use 'nsmul' in names (#6735)

src/algebra/big_operators/basic.lean

@@ -1239,18 +1239,18 @@ lemma count_sum' {s : finset β} {a : α} {f : β → multiset α} :
   count a (∑ x in s, f x) = ∑ x in s, count a (f x) :=
 by { dunfold finset.sum, rw count_sum }
 
-@[simp] lemma to_finset_sum_count_smul_eq (s : multiset α) :
+@[simp] lemma to_finset_sum_count_nsmul_eq (s : multiset α) :
   (∑ a in s.to_finset, s.count a •ℕ (a ::ₘ 0)) = s :=
 begin
   apply ext', intro b,
   rw count_sum',
   have h : count b s = count b (count b s •ℕ (b ::ₘ 0)),
-  { rw [singleton_coe, count_smul, ← singleton_coe, count_singleton, mul_one] },
+  { rw [singleton_coe, count_nsmul, ← singleton_coe, count_singleton, mul_one] },
   rw h, clear h,
   apply finset.sum_eq_single b,
-  { intros c h hcb, rw count_smul, convert mul_zero (count c s),
+  { intros c h hcb, rw count_nsmul, convert mul_zero (count c s),
     apply count_eq_zero.mpr, exact finset.not_mem_singleton.mpr (ne.symm hcb) },
-  { intro hb, rw [count_eq_zero_of_not_mem (mt mem_to_finset.2 hb), count_smul, zero_mul]}
+  { intro hb, rw [count_eq_zero_of_not_mem (mt mem_to_finset.2 hb), count_nsmul, zero_mul]}
 end
 
 theorem exists_smul_of_dvd_count (s : multiset α) {k : ℕ} (h : ∀ (a : α), k ∣ multiset.count a s) :
@@ -1262,7 +1262,7 @@ begin
   { refine congr_arg s.to_finset.sum _,
     apply funext, intro x,
     rw [← mul_nsmul, nat.mul_div_cancel' (h x)] },
-  rw [← finset.sum_nsmul, h₂, to_finset_sum_count_smul_eq]
+  rw [← finset.sum_nsmul, h₂, to_finset_sum_count_nsmul_eq]
 end
 
 end multiset

src/data/finsupp/basic.lean

@@ -1487,7 +1487,7 @@ begin
   { rw [to_multiset_zero, multiset.prod_zero, finsupp.prod_zero_index] },
   { assume a n f _ _ ih,
     rw [to_multiset_add, multiset.prod_add, ih, to_multiset_single, finsupp.prod_add_index,
-      finsupp.prod_single_index, multiset.prod_smul, multiset.singleton_eq_singleton,
+      finsupp.prod_single_index, multiset.prod_nsmul, multiset.singleton_eq_singleton,
       multiset.prod_singleton],
     { exact pow_zero a },
     { exact pow_zero },
@@ -1511,7 +1511,7 @@ end
   f.to_multiset.count a = f a :=
 calc f.to_multiset.count a = f.sum (λx n, (n •ℕ {x} : multiset α).count a) :
     (f.support.sum_hom $ multiset.count a).symm
-  ... = f.sum (λx n, n * ({x} : multiset α).count a) : by simp only [multiset.count_smul]
+  ... = f.sum (λx n, n * ({x} : multiset α).count a) : by simp only [multiset.count_nsmul]
   ... = f.sum (λx n, n * (x ::ₘ 0 : multiset α).count a) : rfl
   ... = f a * (a ::ₘ 0 : multiset α).count a : sum_eq_single _
     (λ a' _ H, by simp only [multiset.count_cons_of_ne (ne.symm H), multiset.count_zero, mul_zero])

src/data/multiset/basic.lean

@@ -423,7 +423,7 @@ def card : multiset α →+ ℕ :=
 theorem card_add (s t : multiset α) : card (s + t) = card s + card t :=
 card.map_add s t
 
-lemma card_smul (s : multiset α) (n : ℕ) :
+lemma card_nsmul (s : multiset α) (n : ℕ) :
   (n •ℕ s).card = n * s.card :=
 by rw [card.map_nsmul s n, nat.nsmul_eq_mul]
 
@@ -827,11 +827,11 @@ quotient.induction_on₂ s t $ λ l₁ l₂, by simp
 instance sum.is_add_monoid_hom [add_comm_monoid α] : is_add_monoid_hom (sum : multiset α → α) :=
 { map_add := sum_add, map_zero := sum_zero }
 
-lemma prod_smul {α : Type*} [comm_monoid α] (m : multiset α) :
+lemma prod_nsmul {α : Type*} [comm_monoid α] (m : multiset α) :
   ∀n, (n •ℕ m).prod = m.prod ^ n
 | 0       := rfl
 | (n + 1) :=
-  by rw [add_nsmul, one_nsmul, pow_add, pow_one, prod_add, prod_smul n]
+  by rw [add_nsmul, one_nsmul, pow_add, pow_one, prod_add, prod_nsmul n]
 
 @[simp] theorem prod_repeat [comm_monoid α] (a : α) (n : ℕ) : prod (multiset.repeat a n) = a ^ n :=
 by simp [repeat, list.prod_repeat]
@@ -1824,7 +1824,7 @@ countp_add _
 instance count.is_add_monoid_hom (a : α) : is_add_monoid_hom (count a : multiset α → ℕ) :=
 countp.is_add_monoid_hom _
 
-@[simp] theorem count_smul (a : α) (n s) : count a (n •ℕ s) = n * count a s :=
+@[simp] theorem count_nsmul (a : α) (n s) : count a (n •ℕ s) = n * count a s :=
 by induction n; simp [*, succ_nsmul', succ_mul]
 
 theorem count_pos {a : α} {s : multiset α} : 0 < count a s ↔ a ∈ s :=

src/data/multiset/fold.lean

@@ -85,7 +85,7 @@ open nat
 theorem le_smul_erase_dup [decidable_eq α] (s : multiset α) :
   ∃ n : ℕ, s ≤ n •ℕ erase_dup s :=
 ⟨(s.map (λ a, count a s)).fold max 0, le_iff_count.2 $ λ a, begin
-  rw count_smul, by_cases a ∈ s,
+  rw count_nsmul, by_cases a ∈ s,
   { refine le_trans _ (mul_le_mul_left _ $ count_pos.2 $ mem_erase_dup.2 h),
     have : count a s ≤ fold max 0 (map (λ a, count a s) (a ::ₘ erase s a));
     [simp [le_max_left], simpa [cons_erase h]] },

src/data/pnat/factors.lean

@@ -345,7 +345,7 @@ begin
   congr' 2,
   apply multiset.eq_repeat.mpr,
   split,
-  { rw [multiset.card_smul, prime_multiset.card_of_prime, mul_one] },
+  { rw [multiset.card_nsmul, prime_multiset.card_of_prime, mul_one] },
   { have : ∀ (m : ℕ), m •ℕ (p ::ₘ 0) = multiset.repeat p m :=
     λ m, by {induction m with m ih, { refl },
              rw [succ_nsmul, multiset.repeat_succ, ih],