no goals
ι : Type ?u.170595
α : Type ?u.170598
β : Type ?u.170601
γ : Type ?u.170604
s : Multiset ℕ
n : ℕ
⊢ prod s % n = prod (map (fun x => x % n) s) % n
induction s using Multiset.induction <;> simp [Nat.mul_mod, *]