mathlib documentation

algebra.big_operators.part_enat

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))