ι : Type ?u.22722
α : Type ?u.22725
M : Type u_1
N : Type u_3
P : Type ?u.22734
M₀ : Type ?u.22737
G : Type ?u.22740
R : Type ?u.22743
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List M
F : Type u_2
inst✝ : MonoidHomClass F M N
f : F
⊢ foldl (fun x y => x * ↑f y) (↑f 1) l = ↑f (foldl (fun x x_1 => x * x_1) 1 l)
ι : Type ?u.22722
α : Type ?u.22725
M : Type u_1
N : Type u_3
P : Type ?u.22734
M₀ : Type ?u.22737
G : Type ?u.22740
R : Type ?u.22743
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List M
F : Type u_2
inst✝ : MonoidHomClass F M N
f : F
⊢ prod (map (↑f) l) = ↑f (prod l)
simp only [prod, foldl_map, ← map_one f]
no goals
ι : Type ?u.22722
α : Type ?u.22725
M : Type u_1
N : Type u_3
P : Type ?u.22734
M₀ : Type ?u.22737
G : Type ?u.22740
R : Type ?u.22743
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List M
F : Type u_2
inst✝ : MonoidHomClass F M N
f : F
⊢ foldl (fun x y => x * ↑f y) (↑f 1) l = ↑f (foldl (fun x x_1 => x * x_1) 1 l)
exact l.foldl_hom f (. * .) (. * f .) 1 (fun x y => (map_mul f x y).symm)