Theorems · Theorem · group theory
Set.list_sum_mem_list_sum
∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (t : List ι) (f : ι → Set α) (g : ι → α),
(∀ i ∈ t, g i ∈ f i) → (List.map g t).sum ∈ (List.map f t).sumAn n-ary version of Set.add_mem_add.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses propext
- Assumes
- AddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- Set.addstatement · cited by 338
- Set.zerostatement · cited by 87
- Set.add_mem_addproof · cited by 30
- Set.mem_zeroproof · cited by 6
Cited by1
Results whose statement or proof uses this declaration.
- Set.multiset_sum_mem_multiset_sumproof · cited by 1