Theorems · Theorem · group theory
Finset.sum_erase_add
∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (f : ι → M) {a : ι},
a ∈ s → ∑ x ∈ s.erase a, f x + f a = ∑ x ∈ s, f xA variant of Finset.add_sum_erase with the addition swapped.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 58 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.
Cites6
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
- add_commproof · cited by 1,535
- Finset.erasestatement and proof · cited by 455
- Finset.add_sum_eraseproof · cited by 28
Cited by13
Results whose statement or proof uses this declaration.
- MonovaryOn.sum_smul_comp_perm_le_sum_smulproof · cited by 7
- Finset.sum_erase_eq_subproof · cited by 6
- MonovaryOn.sum_smul_comp_perm_eq_sum_smul_iffproof · cited by 5
- ZSpan.fundamentalDomain_ae_parallelepipedproof · cited by 2
- harmonic_le_one_add_logproof · cited by 1
- IsLinearSet.isProperSemilinearSetproof · cited by 1
- Affine.Simplex.closedInterior_eq_interior_unionproof · cited by 1
- Module.exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_cardproof · cited by 1
- Affine.Simplex.closedInterior_inter_shift_zeroproof · cited by 1
- HahnEmbedding.Seed.baseEmbedding_posproof · cited by 1
- Transcendental.linearIndependent_sub_invproof · cited by 1
- ZMod.exists_one_add_mul_pow_prime_eqproof · cited by 0