Big operators in `enat` #

A simple lemma about sums in enat.

theorem finset.sum_nat_coe_enat {α : Type u_1} (s : finset α) (f : α → ℕ) :

∑ (x : α) in s, ↑(f x) = ↑∑ (x : α) in s, f x

Big operators in enat #