Theorems · Theorem · group theory
Finset.noncommSum_union_of_disjoint
∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] [inst_1 : DecidableEq α] {s t : Finset α},
Disjoint s t →
∀ (f : α → β) (comm : (↑(s ∪ t)).Pairwise (Function.onFun AddCommute f)),
(s ∪ t).noncommSum f comm = s.noncommSum f ⋯ + t.noncommSum f ⋯The non-commutative version of Finset.sum_union
- Defined in
- Mathlib.Data.Finset.NoncommProd
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddMonoidDecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites26
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Finsetstatement and proof · cited by 13,712
- SetLike.coestatement and proof · cited by 8,199
- Set.ofPredproof · cited by 6,101
- AddMonoidstatement and proof · cited by 2,864
- Multisetproof · cited by 2,627
- Disjointstatement and proof · cited by 2,201
- Multiset.mapproof · cited by 876
- Function.onFunstatement and proof · cited by 570
- Finset.valproof · cited by 438
- Set.Pairwisestatement and proof · cited by 321
- Multiset.ofListproof · cited by 290
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.