no goals
α : Type u_1
β : Type ?u.8870
γ : Type ?u.8873
δ : Type ?u.8876
inst✝ : CommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : p ∣ Multiset.prod s → ∃ a, a ∈ s ∧ p ∣ a
h : p ∣ Multiset.prod (a ::ₘ s)
⊢ p ∣ a * Multiset.prod s
simpa using h