Big-operator lemmas

Auxiliary material for the formalization of M. Stoll, Galois groups over ℚ of some iterated polynomials, Arch. Math. 59 (1992), 239-244; upstreaming candidates for Mathlib.

theorem Finset.sum_mul_ite_const {ι : Type u_1} {R : Type u_2} [CommSemiring R] (s : Finset ι) (p : ι → Prop) [DecidablePred p] (g : ι → R) (c : R) : (∑ x ∈ s, g x * if p x then c else 0) = c * ∑ x ∈ s with p x, g x

Factor a constant out of an indicator-weighted sum: ∑ g x · [p x]·c = c · ∑_{p x} g x.

theorem sum_zmod_two_smul_eq_sum_filter {ι : Type u_1} {M : Type u_2} [Fintype ι] [AddCommMonoid M] [Module (ZMod 2) M] (m : ι → M) (g : ι → ZMod 2) : ∑ i : ι, g i • m i = ∑ i : ι with g i = 1, m i

An 𝔽₂-linear combination is the sum over the support of the coefficient function.