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 (Finset.filter (fun (x : ι) => Odd (f x)) s).card

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