α : Type u_1
β : Type ?u.10567
ι : Type ?u.10570
a : α
n : ℕ
⊢ 0 • {a} = 0
α : Type u_1
β : Type ?u.10567
ι : Type ?u.10570
a : α
n : ℕ
⊢ ↑toMultiset (single a n) = n • {a}
rw [toMultiset_apply, sum_single_index]
no goals
α : Type u_1
β : Type ?u.10567
ι : Type ?u.10570
a : α
n : ℕ
⊢ 0 • {a} = 0
apply zero_nsmul