case h.e'_2.h.e'_3
ι : Type u_2
α : Type u_1
β : Type ?u.99606
γ : Type ?u.99609
inst✝ : DivisionCommMonoid α
m : Multiset ι
f g : ι → α
n : ℤ
⊢ map (fun i => f i ^ n) m = map (↑(zpowGroupHom n)) (map f m)
ι : Type u_2
α : Type u_1
β : Type ?u.99606
γ : Type ?u.99609
inst✝ : DivisionCommMonoid α
m : Multiset ι
f g : ι → α
n : ℤ
⊢ prod (map (fun i => f i ^ n) m) = prod (map f m) ^ n
convert (m.map f).prod_hom (zpowGroupHom n : α →* α)
no goals
case h.e'_2.h.e'_3
ι : Type u_2
α : Type u_1
β : Type ?u.99606
γ : Type ?u.99609
inst✝ : DivisionCommMonoid α
m : Multiset ι
f g : ι → α
n : ℤ
⊢ map (fun i => f i ^ n) m = map (↑(zpowGroupHom n)) (map f m)
simp only [map_map, Function.comp_apply, zpowGroupHom_apply]