α : Type u_1
β : Type ?u.16742
γ : Type ?u.16745
s : Multiset α
l : List α
H : ∀ (x : α), ¬x ∈ Quot.mk Setoid.r l
⊢ Quot.mk Setoid.r [] = 0
α : Type u_1
β : Type ?u.16742
γ : Type ?u.16745
s : Multiset α
l : List α
H : ∀ (x : α), ¬x ∈ Quot.mk Setoid.r l
⊢ Quot.mk Setoid.r l = 0
rw [eq_nil_iff_forall_not_mem.mpr H]
no goals
α : Type u_1
β : Type ?u.16742
γ : Type ?u.16745
s : Multiset α
l : List α
H : ∀ (x : α), ¬x ∈ Quot.mk Setoid.r l
⊢ Quot.mk Setoid.r [] = 0
rfl