ι : Type ?u.90765
α : Type u_1
β : Type ?u.90771
γ : Type ?u.90774
inst✝² : CommMonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
s : Multiset α
l : List α
⊢ List.prod l = 0 ↔ 0 ∈ ↑l
ι : Type ?u.90765
α : Type u_1
β : Type ?u.90771
γ : Type ?u.90774
inst✝² : CommMonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
s : Multiset α
l : List α
⊢ prod (Quotient.mk (List.isSetoid α) l) = 0 ↔ 0 ∈ Quotient.mk (List.isSetoid α) l
rw [quot_mk_to_coe, coe_prod]
no goals
ι : Type ?u.90765
α : Type u_1
β : Type ?u.90771
γ : Type ?u.90774
inst✝² : CommMonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
s : Multiset α
l : List α
⊢ List.prod l = 0 ↔ 0 ∈ ↑l
exact List.prod_eq_zero_iff