Mathlib Map

Theorems · Theorem · group theory

Finset.sum_insert_zero

∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [inst : AddCommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι],
  f a = 0 → ∑ x ∈ insert a s, f x = ∑ x ∈ s, f x

The sum of f over insert a s is the same as the sum over s, as long as f a = 0.

Defined in
Mathlib.Algebra.BigOperators.Group.Finset.Basic
Cited by
2 results in Mathlib
Foundations
Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddCommMonoidDecidableEq
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Finset.weightedVSubOfPoint_insert · cited by 3Finset.weightedVSubOfPoin…mem_vectorSpan_iff_eq_weightedVSub · cited by 1mem_vectorSpan_iff_eq_wei…Finset · cited by 13712FinsetAddCommMonoid · cited by 12281AddCommMonoidFinset.sum · cited by 5195Finset.sumFinset.sum_insert_of_eq_zero_if_notMem · cited by 3Finset.sum_insert_of_eq_z…Finset.sum_insert_zeroCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.