Theorems · Theorem · group theory
Finset.sum_filter_add_sum_filter_not
∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] (s : Finset ι) (p : ι → Prop) [inst_1 : DecidablePred p]
[inst_2 : (x : ι) → Decidable ¬p x] (f : ι → M), ∑ x ∈ s with p x, f x + ∑ x ∈ s with ¬p x, f x = ∑ x ∈ s, f x- Cited by
- 20 results in Mathlib
- Foundations
- Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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.filterstatement · cited by 949
- Classical.decEqproof · cited by 134
- Finset.sum_unionproof · cited by 40
- Finset.filter_union_filter_not_eqproof · cited by 16
- Finset.disjoint_filter_filter_notproof · cited by 6
Cited by20
Results whose statement or proof uses this declaration.
- Finset.sum_indicator_eq_sum_filterproof · cited by 5
- IsNilpotent.exp_add_of_commuteproof · cited by 3
- Fin.sum_sum_eq_sum_triangle_addproof · cited by 2
- AffineIndependent.affineIndependent_of_notMem_spanproof · cited by 2
- Finset.sum_apply_diteproof · cited by 2
- BoxIntegral.HasIntegral.of_bRiemann_eq_false_of_forall_isLittleOproof · cited by 2
- Finpartition.IsEquipartition.card_large_parts_eq_modproof · cited by 2
- Finset.indicator_biUnion_eq_sum_powersetproof · cited by 1
- Finset.sum_filter_not_add_sum_filterproof · cited by 1
- Convex.radon_partitionproof · cited by 1
- MeasureTheory.SignedMeasure.exists_subset_lt_enorm_apply_of_lt_variationproof · cited by 1
- linearIndependent_iffₒₛproof · cited by 1