Big operators in `part_enat` #

A simple lemma about sums in part_enat.

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

s.sum (λ (x : α), ↑(f x)) = ↑(s.sum (λ (x : α), f x))

Big operators in part_enat #