no goals
α : Type u_1
β : Type ?u.112914
γ : Type ?u.112917
ι : Type ?u.112920
inst✝ : SeminormedRing α
l : List α
hl : l ≠ []
⊢ prod (map norm l) = (fun a => ↑a) (prod (map nnnorm l))
simp [NNReal.coe_list_prod, List.map_map]