Theorems · Theorem · group theory
Finset.add_sum_erase
∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (f : ι → M) {a : ι},
a ∈ s → f a + ∑ x ∈ s.erase a, f x = ∑ x ∈ s, f xTaking a sum over s : Finset ι is the same as adding the value on a single
element f a to the sum over s.erase a.
See Multiset.sum_map_erase for the Multiset version.
- Cited by
- 28 results in Mathlib
- Foundations
- Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommMonoidDecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- Finset.sumstatement and proof · cited by 5,195
- Finset.erasestatement · cited by 455
- Finset.sum_insertproof · cited by 196
- Finset.insert_eraseproof · cited by 65
- Finset.notMem_eraseproof · cited by 59
Cited by28
Results whose statement or proof uses this declaration.
- Finset.sum_erase_addproof · cited by 13
- Lagrange.eval_interpolate_at_nodeproof · cited by 5
- AlgebraicTopology.DoldKan.decomposition_Qproof · cited by 4
- Lagrange.sum_basisproof · cited by 3
- Ideal.IsHomogeneous.isPrime_of_homogeneous_mem_or_memproof · cited by 3
- Finsupp.mapDomain_apply'proof · cited by 3
- Matrix.det_updateRow_sumproof · cited by 3
- iSupIndep_iff_finsetSum_eq_zero_imp_eq_zeroproof · cited by 3
- Finsupp.multinomial_updateproof · cited by 2
- Fin.accumulate_recproof · cited by 2
- dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAtproof · cited by 1
- Hindman.FS.finsetSumproof · cited by 1