Theorems · Theorem · group theory
Multiset.noncommSum_coe
∀ {α : Type u_3} [inst : AddMonoid α] (l : List α) (comm : {x | x ∈ ↑l}.Pairwise AddCommute),
(↑l).noncommSum comm = l.sum- Defined in
- Mathlib.Data.Finset.NoncommProd
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 23 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddMonoid
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.
- Set.ofPredstatement and proof · cited by 6,101
- AddMonoidstatement and proof · cited by 2,864
- Multisetstatement · cited by 2,627
- Set.Pairwisestatement and proof · cited by 321
- Multiset.ofListstatement and proof · cited by 290
- AddCommutestatement and proof · cited by 185
- Multiset.noncommSumstatement · cited by 18
- Multiset.noncommFold_coeproof · cited by 4
Cited by11
Results whose statement or proof uses this declaration.
- AddSubmonoid.multiset_noncommSum_memproof · cited by 2
- Multiset.noncommSum_addCommuteproof · cited by 1
- Multiset.noncommSum_consproof · cited by 1
- Multiset.noncommSum_cons'proof · cited by 1
- Multiset.noncommSum_eq_card_nsmulproof · cited by 1
- Multiset.noncommSum_inductionproof · cited by 1
- Multiset.map_noncommSumproof · cited by 1
- Finset.noncommSum_union_of_disjointproof · cited by 0
- Multiset.noncommSum_addproof · cited by 0
- Multiset.noncommSum_eq_sumproof · cited by 0
- Finset.noncommSum_toFinsetproof · cited by 0