no goals
α : Type u_1
β : Type ?u.115517
γ : Type ?u.115520
ι : Type ?u.115523
inst✝¹ : SeminormedRing α
inst✝ : NormOneClass α
l : List α
⊢ prod (map norm l) = (fun a => ↑a) (prod (map nnnorm l))
simp [NNReal.coe_list_prod, List.map_map]