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

theorem Finset.card_preimage_eq_sum_card_image_eq {ι : Type u_1} {M : Type u_2} {f : ι → M} {s : Finset M} (hb : ∀ b ∈ s, {a : ι | f a = b}.Finite) : Nat.card ↑(f ⁻¹' ↑s) = ∑ b ∈ s, Nat.card { a : ι // f a = b }