Theorems · Theorem · group theory
Finset.sum_set_coe
∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] {f : ι → M} (s : Set ι) [inst_1 : Fintype ↑s],
∑ i, f ↑i = ∑ i ∈ s.toFinset, f i- Cited by
- 2 results in Mathlib
- Foundations
- Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommMonoidFintype
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- AddCommMonoidstatement and proof · cited by 12,281
- Fintypestatement and proof · cited by 7,736
- Set.Elemstatement and proof · cited by 7,166
- Finset.sumstatement · cited by 5,195
- Finset.univstatement · cited by 3,473
- Set.toFinsetstatement and proof · cited by 217
- Set.mem_toFinsetproof · cited by 47
- Finset.sum_subtypeproof · cited by 11
Cited by2
Results whose statement or proof uses this declaration.
- BoxIntegral.unitPartition.integralSum_eq_tsum_divproof · cited by 1
- Group.card_center_add_sum_card_noncenter_eq_cardproof · cited by 0