ι : Type ?u.327698
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
r : β → γ → Prop
f : α → β
g : α → γ
s : Finset α
h₁ : r 1 1
h₂ : ∀ (a : α) (b : β) (c : γ), r b c → r (f a * b) (g a * c)
⊢ r (Multiset.prod (Multiset.map (fun x => f x) s.val)) (Multiset.prod (Multiset.map (fun x => g x) s.val))
ι : Type ?u.327698
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
r : β → γ → Prop
f : α → β
g : α → γ
s : Finset α
h₁ : r 1 1
h₂ : ∀ (a : α) (b : β) (c : γ), r b c → r (f a * b) (g a * c)
⊢ r (∏ x in s, f x) (∏ x in s, g x)
delta Finset.prod
no goals
ι : Type ?u.327698
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
r : β → γ → Prop
f : α → β
g : α → γ
s : Finset α
h₁ : r 1 1
h₂ : ∀ (a : α) (b : β) (c : γ), r b c → r (f a * b) (g a * c)
⊢ r (Multiset.prod (Multiset.map (fun x => f x) s.val)) (Multiset.prod (Multiset.map (fun x => g x) s.val))
apply Multiset.prod_hom_rel <;> assumption