Theorems · Theorem · group theory
Finset.sum_union
∀ {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [inst : AddCommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι],
Disjoint s₁ s₂ → ∑ x ∈ s₁ ∪ s₂, f x = ∑ x ∈ s₁, f x + ∑ x ∈ s₂, f x- Cited by
- 40 results in Mathlib
- Foundations
- Depth 64 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
- add_zeroproof · cited by 2,707
- Disjointstatement and proof · cited by 2,201
- Finset.disjoint_iff_inter_eq_emptyproof · cited by 4
- Finset.sum_union_interproof · cited by 4
Cited by40
Results whose statement or proof uses this declaration.
- Finset.sum_le_sum_of_subset_of_nonnegproof · cited by 31
- Finset.sum_filter_add_sum_filter_notproof · cited by 20
- Finset.sum_sdiffproof · cited by 16
- Finset.sum_Ico_consecutiveproof · cited by 10
- cauchySeq_finset_iff_sum_vanishingproof · cited by 5
- HasSum.nat_add_neg_add_oneproof · cited by 5
- linearIndependent_sumproof · cited by 3
- Finset.sum_powerset_insertproof · cited by 2
- Finset.sum_sdiff_eq_sum_sdiff_iffproof · cited by 2
- FormalMultilinearSeries.comp_rightInv_aux1proof · cited by 2
- Finset.sum_le_sum_of_ne_zeroproof · cited by 2
- ArithmeticFunction.vonMangoldt_sumproof · cited by 2