Big operators on a finset in the natural numbers

This file contains the results concerning the interaction of finset big operators with natural numbers.

theorem Finset.even_sum_iff_even_card_odd {ι : Type u_1} {s : Finset ι} (f : ι → ℕ) : Even (∑ i ∈ s, f i) ↔ Even {x ∈ s | Odd (f x)}.card

theorem Finset.odd_sum_iff_odd_card_odd {ι : Type u_1} {s : Finset ι} (f : ι → ℕ) : Odd (∑ i ∈ s, f i) ↔ Odd {x ∈ s | Odd (f x)}.card