ι : Type ?u.877667
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
s : Finset α
n : ℤ
f : α → ℤ
⊢ Multiset.prod (Multiset.map ((fun x => x % n) ∘ fun i => f i) s.val) % n =
    Multiset.prod (Multiset.map (fun i => f i % n) s.val) % n
ι : Type ?u.877667
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
s : Finset α
n : ℤ
f : α → ℤ
⊢ Multiset.prod (Multiset.map (fun x => x % n) (Multiset.map (fun i => f i) s.val)) % n = (∏ i in s, f i % n) % n
rw [Finset.prod, Multiset.map_map]
no goals
ι : Type ?u.877667
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
s : Finset α
n : ℤ
f : α → ℤ
⊢ Multiset.prod (Multiset.map ((fun x => x % n) ∘ fun i => f i) s.val) % n =
    Multiset.prod (Multiset.map (fun i => f i % n) s.val) % n
rfl