no goals
R : Type u_1
ι : Type ?u.17742
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
l : Multiset R
⊢ Multiset.sum l * Multiset.sum l = Multiset.sum (Multiset.map (fun x => x * x) l)
simp_rw [← pow_two, multiset_sum_sq]