Characteristic two and big operators over Finset

We prove several lemmas about sums over monoids and ring of characteristic two.

Extra lemmas

theorem IMOSL.Extra.symmDiff_singleton_eq_insert {ι : Type u_1} [DecidableEq ι] {i : ι} {S : Finset ι} (h : i ∉ S) : symmDiff {i} S = insert i S

theorem IMOSL.Extra.symmDiff_singleton_eq_erase {ι : Type u_1} [DecidableEq ι] {i : ι} {S : Finset ι} (h : i ∈ S) : symmDiff {i} S = S.erase i

CharTwo

theorem IMOSL.Extra.CharTwo.symmDiff_singleton_sum_eq {M : Type u_2} {ι : Type u_1} [AddCommMonoid M] [CharTwo M] [DecidableEq ι] (f : ι → M) (i : ι) (S : Finset ι) : (symmDiff {i} S).sum f = f i + S.sum f

theorem IMOSL.Extra.CharTwo.symmDiff_sum_eq {M : Type u_2} {ι : Type u_1} [AddCommMonoid M] [CharTwo M] [DecidableEq ι] (f : ι → M) (S T : Finset ι) : (symmDiff S T).sum f = S.sum f + T.sum f