Documentation

Mathlib.Algebra.BigOperators.Ring.Nat

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