Powers of extended nonnegative reals to a sum

A power of an extended nonnegative real to a sum of nonnegative exponents is the product of the powers, as for the reals.

[UPSTREAM] candidate for Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean, beside ENNReal.prod_rpow_of_nonneg.

theorem ENNReal.rpow_sum_of_nonneg {ι : Type u_1} {s : Finset ι} {w : ι → ℝ} (x : ENNReal) (hw : ∀ i ∈ s, 0 ≤ w i) : x ^ ∑ i ∈ s, w i = ∏ i ∈ s, x ^ w i