no goals
ι : Type ?u.172491
α : Type ?u.172494
β : Type ?u.172497
γ : Type ?u.172500
s : Multiset ℤ
n : ℤ
⊢ prod s % n = prod (map (fun x => x % n) s) % n
induction s using Multiset.induction <;> simp [Int.mul_emod, *]