ι : Type ?u.14945
α : Type u_1
β : Type ?u.14951
γ : Type ?u.14954
inst✝ : CommMonoid α
s t : Multiset α
a : α
m✝ : Multiset ι
f g : ι → α
m : Multiset α
⊢ prod 0 = 1
ι : Type ?u.14945
α : Type u_1
β : Type ?u.14951
γ : Type ?u.14954
inst✝ : CommMonoid α
s t : Multiset α
a : α
m✝ : Multiset ι
f g : ι → α
m : Multiset α
⊢ prod (0 • m) = prod m ^ 0
rw [zero_nsmul, pow_zero]
no goals
ι : Type ?u.14945
α : Type u_1
β : Type ?u.14951
γ : Type ?u.14954
inst✝ : CommMonoid α
s t : Multiset α
a : α
m✝ : Multiset ι
f g : ι → α
m : Multiset α
⊢ prod 0 = 1
rfl
no goals
ι : Type ?u.14945
α : Type u_1
β : Type ?u.14951
γ : Type ?u.14954
inst✝ : CommMonoid α
s t : Multiset α
a : α
m✝ : Multiset ι
f g : ι → α
m : Multiset α
n : ℕ
⊢ prod ((n + 1) • m) = prod m ^ (n + 1)
rw [add_nsmul, one_nsmul, pow_add, pow_one, prod_add, prod_nsmul m n]