mathlib documentation

algebra.big_operators.enat

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