Theorems · Theorem · group theory
Finset.sum_attach
∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] (s : Finset ι) (f : ι → M), ∑ x ∈ s.attach, f ↑x = ∑ x ∈ s, f x- Cited by
- 54 results in Mathlib
- Foundations
- Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommMonoid
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
- Function.Injective.injOnproof · cited by 280
- Subtype.coe_injectiveproof · cited by 205
- Finset.attachstatement · cited by 168
- Finset.sum_imageproof · cited by 26
- Finset.attach_image_valproof · cited by 6
Cited by54
Results whose statement or proof uses this declaration.
- Finset.sum_coe_sortproof · cited by 24
- Fin.sum_univ_eq_sum_rangeproof · cited by 10
- Finset.tsum_subtypeproof · cited by 7
- Finset.sum_ite_of_falseproof · cited by 6
- Finset.hasSumproof · cited by 6
- InnerProductSpace.gramSchmidt_defproof · cited by 5
- Ideal.sum_ramification_inertiaproof · cited by 4
- linearIndepOn_finset_iffproof · cited by 4
- MeasureTheory.measure_biUnion_finset₀proof · cited by 4
- HasFDerivAt.finsetProdproof · cited by 3
- Finset.tsum_subtype'proof · cited by 3
- MvPowerSeries.coeff_prodproof · cited by 3