Loogle!
Result
Found 2849 declarations mentioning Finset.sum. Of these, only the first 200 are shown.
- Finset.sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : α → β) : β - Finset.sum_val 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} [AddCommMonoid α] (s : Finset α) : s.val.sum = s.sum id - Finset.sum.eq_1 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : α → β) : s.sum f = (Multiset.map f s.val).sum - Finset.sum_multiset_singleton 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} (s : Finset α) : ∑ a ∈ s, {a} = s.val - Finset.sum_eq_multiset_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : α → β) : ∑ x ∈ s, f x = (Multiset.map f s.val).sum - Finset.sum_map_val 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : α → β) : (Multiset.map f s.val).sum = ∑ a ∈ s, f a - Finset.sum_mk 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Multiset α) (hs : s.Nodup) (f : α → β) : { val := s, nodup := hs }.sum f = (Multiset.map f s).sum - Finset.sum_empty 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} {f : α → β} [AddCommMonoid β] : ∑ x ∈ ∅, f x = 0 - Finset.sum_of_isEmpty 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} {f : α → β} [AddCommMonoid β] [IsEmpty α] (s : Finset α) : ∑ i ∈ s, f i = 0 - Finset.sum_range_zero 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{β : Type u_4} [AddCommMonoid β] (f : ℕ → β) : ∑ k ∈ Finset.range 0, f k = 0 - Finset.nonempty_of_sum_ne_zero 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] (h : ∑ x ∈ s, f x ≠ 0) : s.Nonempty - Finset.sum_toList 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_6} [AddCommMonoid α] (s : Finset α) : s.toList.sum = ∑ x ∈ s, x - Finset.op_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} (f : α → β) : MulOpposite.op (∑ x ∈ s, f x) = ∑ x ∈ s, MulOpposite.op (f x) - Finset.unop_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} (f : α → βᵐᵒᵖ) : MulOpposite.unop (∑ x ∈ s, f x) = ∑ x ∈ s, MulOpposite.unop (f x) - Fintype.sum_empty 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_9} {β : Type u_10} [AddCommMonoid β] [IsEmpty α] [Fintype α] (f : α → β) : ∑ x, f x = 0 - Multiset.card_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {α : Type u_3} (s : Finset ι) (f : ι → Multiset α) : (∑ i ∈ s, f i).card = ∑ i ∈ s, (f i).card - Finset.sum_const_zero 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] : ∑ _x ∈ s, 0 = 0 - Finset.sum_map_toList 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : α → β) : (List.map f s.toList).sum = s.sum f - Finset.sum_to_list 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : α → β) : (List.map f s.toList).sum = s.sum f - Function.Bijective.sum_comp 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] {e : ι → κ} (he : Function.Bijective e) (g : κ → α) : ∑ i, g (e i) = ∑ i, g i - Multiset.count_sum' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} [DecidableEq α] {s : Finset β} {a : α} {f : β → Multiset α} : Multiset.count a (∑ x ∈ s, f x) = ∑ x ∈ s, Multiset.count a (f x) - Finset.sum_filter_count_eq_countP 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} [DecidableEq α] (p : α → Prop) [DecidablePred p] (l : List α) : ∑ x ∈ {x ∈ l.toFinset | p x}, List.count x l = List.countP (fun b => decide (p b)) l - Finset.sum_map 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (s : Finset α) (e : α ↪ γ) (f : γ → β) : ∑ x ∈ Finset.map e s, f x = ∑ x ∈ s, f (e x) - Equiv.sum_comp 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] (e : ι ≃ κ) (g : κ → α) : ∑ i, g (e i) = ∑ i, g i - Finset.sum_int_mod 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} (s : Finset α) (n : ℤ) (f : α → ℤ) : (∑ i ∈ s, f i) % n = (∑ i ∈ s, f i % n) % n - Finset.sum_nat_mod 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} (s : Finset α) (n : ℕ) (f : α → ℕ) : (∑ i ∈ s, f i) % n = (∑ i ∈ s, f i % n) % n - Multiset.disjoint_finset_sum_left 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_6} {i : Finset β} {f : β → Multiset α} {a : Multiset α} : Disjoint (i.sum f) a ↔ ∀ b ∈ i, Disjoint (f b) a - Multiset.disjoint_finset_sum_right 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_6} {i : Finset β} {f : β → Multiset α} {a : Multiset α} : Disjoint a (i.sum f) ↔ ∀ b ∈ i, Disjoint a (f b) - Finset.sum_ite_index 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} [AddCommMonoid β] (p : Prop) [Decidable p] (s t : Finset α) (f : α → β) : ∑ x ∈ if p then s else t, f x = if p then ∑ x ∈ s, f x else ∑ x ∈ t, f x - Finset.sum_ite_irrel 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} [AddCommMonoid β] (p : Prop) [Decidable p] (s : Finset α) (f g : α → β) : (∑ x ∈ s, if p then f x else g x) = if p then ∑ x ∈ s, f x else ∑ x ∈ s, g x - Fintype.sum_bijective 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] (e : ι → κ) (he : Function.Bijective e) (f : ι → α) (g : κ → α) (h : ∀ (x : ι), f x = g (e x)) : ∑ x, f x = ∑ x, g x - Function.Bijective.finset_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] (e : ι → κ) (he : Function.Bijective e) (f : ι → α) (g : κ → α) (h : ∀ (x : ι), f x = g (e x)) : ∑ x, f x = ∑ x, g x - Finset.sum_neg_distrib 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [SubtractionCommMonoid β] : ∑ x ∈ s, -f x = -∑ x ∈ s, f x - Finset.sum_nsmul 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (n : ℕ) (f : α → β) : ∑ x ∈ s, n • f x = n • ∑ x ∈ s, f x - Finset.sum_induction_nonempty 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {s : Finset α} {M : Type u_6} [AddCommMonoid M] (f : α → M) (p : M → Prop) (hom : ∀ (a b : M), p a → p b → p (a + b)) (nonempty : s.Nonempty) (base : ∀ x ∈ s, p (f x)) : p (∑ x ∈ s, f x) - Fintype.sum_equiv 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] (e : ι ≃ κ) (f : ι → α) (g : κ → α) (h : ∀ (x : ι), f x = g (e x)) : ∑ x, f x = ∑ x, g x - ofAdd_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {α : Type u_3} [AddCommMonoid α] (s : Finset ι) (f : ι → α) : Multiplicative.ofAdd (∑ i ∈ s, f i) = ∏ i ∈ s, Multiplicative.ofAdd (f i) - ofMul_prod 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {α : Type u_3} [CommMonoid α] (s : Finset ι) (f : ι → α) : Additive.ofMul (∏ i ∈ s, f i) = ∑ i ∈ s, Additive.ofMul (f i) - Finset.ite_sum_zero 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} [AddCommMonoid β] (p : Prop) [Decidable p] (s : Finset α) (f : α → β) : (if p then ∑ x ∈ s, f x else 0) = ∑ x ∈ s, if p then f x else 0 - Finset.ite_zero_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} [AddCommMonoid β] (p : Prop) [Decidable p] (s : Finset α) (f : α → β) : (if p then 0 else ∑ x ∈ s, f x) = ∑ x ∈ s, if p then 0 else f x - Finset.sum_zsmul 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} [SubtractionCommMonoid β] (f : α → β) (s : Finset α) (n : ℤ) : ∑ a ∈ s, n • f a = n • ∑ a ∈ s, f a - toAdd_prod 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {α : Type u_3} [AddCommMonoid α] (s : Finset ι) (f : ι → Multiplicative α) : Multiplicative.toAdd (∏ i ∈ s, f i) = ∑ i ∈ s, Multiplicative.toAdd (f i) - toMul_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {α : Type u_3} [CommMonoid α] (s : Finset ι) (f : ι → Additive α) : Additive.toMul (∑ i ∈ s, f i) = ∏ i ∈ s, Additive.toMul (f i) - Finset.sum_dite_irrel 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} [AddCommMonoid β] (p : Prop) [Decidable p] (s : Finset α) (f : p → α → β) (g : ¬p → α → β) : (∑ x ∈ s, if h : p then f h x else g h x) = if h : p then ∑ x ∈ s, f h x else ∑ x ∈ s, g h x - Equiv.Perm.sum_comp 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} [AddCommMonoid β] (σ : Equiv.Perm α) (s : Finset α) (f : α → β) (hs : {a | σ a ≠ a} ⊆ ↑s) : ∑ x ∈ s, f (σ x) = ∑ x ∈ s, f x - map_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] [AddCommMonoid γ] {G : Type u_6} [FunLike G β γ] [AddMonoidHomClass G β γ] (g : G) (f : α → β) (s : Finset α) : g (∑ x ∈ s, f x) = ∑ x ∈ s, g (f x) - Finset.sum_induction 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {s : Finset α} {M : Type u_6} [AddCommMonoid M] (f : α → M) (p : M → Prop) (hom : ∀ (a b : M), p a → p b → p (a + b)) (unit : p 0) (base : ∀ x ∈ s, p (f x)) : p (∑ x ∈ s, f x) - Finset.sum_sub_distrib 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} {s : Finset α} {f g : α → β} [SubtractionCommMonoid β] : ∑ x ∈ s, (f x - g x) = ∑ x ∈ s, f x - ∑ x ∈ s, g x - Finset.sum_bijective 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (e : ι → κ) (he : Function.Bijective e) (hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) : ∑ i ∈ s, f i = ∑ i ∈ t, g i - Equiv.Perm.sum_comp' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} [AddCommMonoid β] (σ : Equiv.Perm α) (s : Finset α) (f : α → α → β) (hs : {a | σ a ≠ a} ⊆ ↑s) : ∑ x ∈ s, f (σ x) x = ∑ x ∈ s, f x ((Equiv.symm σ) x) - Finset.sum_nbij 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (i_inj : Set.InjOn i ↑s) (i_surj : Set.SurjOn i ↑s ↑t) (h : ∀ a ∈ s, f a = g (i a)) : ∑ x ∈ s, f x = ∑ x ∈ t, g x - Finset.sum_attach_univ 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [Fintype ι] (f : { i // i ∈ Finset.univ } → α) : ∑ i ∈ Finset.univ.attach, f i = ∑ i, f ⟨i, ⋯⟩ - Finset.sum_equiv 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (e : ι ≃ κ) (hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) : ∑ i ∈ s, f i = ∑ i ∈ t, g i - Finset.sum_coe_sort_eq_attach 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} (s : Finset α) [AddCommMonoid β] (f : { x // x ∈ s } → β) : ∑ i, f i = ∑ i ∈ s.attach, f i - Finset.sum_hom_rel 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] [AddCommMonoid γ] {r : β → γ → Prop} {f : α → β} {g : α → γ} {s : Finset α} (h₁ : r 0 0) (h₂ : ∀ (a : α) (b : β) (c : γ), r b c → r (f a + b) (g a + c)) : r (∑ x ∈ s, f x) (∑ x ∈ s, g x) - Finset.sum_mem_multiset 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (m : Multiset α) (f : { x // x ∈ m } → β) (g : α → β) (hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x) : ∑ x, f x = ∑ x ∈ m.toFinset, g x - Finset.sum_nbij' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (i : ι → κ) (j : κ → ι) (hi : ∀ a ∈ s, i a ∈ t) (hj : ∀ a ∈ t, j a ∈ s) (left_inv : ∀ a ∈ s, j (i a) = a) (right_inv : ∀ a ∈ t, i (j a) = a) (h : ∀ a ∈ s, f a = g (i a)) : ∑ x ∈ s, f x = ∑ x ∈ t, g x - Finset.sum_erase_attach 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [DecidableEq ι] {s : Finset ι} (f : ι → α) (i : { x // x ∈ s }) : ∑ j ∈ s.attach.erase i, f ↑j = ∑ j ∈ s.erase ↑i, f j - Finset.sum_bij 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (i : (a : ι) → a ∈ s → κ) (hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t) (i_inj : ∀ (a₁ : ι) (ha₁ : a₁ ∈ s) (a₂ : ι) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) (i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b) (h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)) : ∑ x ∈ s, f x = ∑ x ∈ t, g x - Finset.sum_bij' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (i : (a : ι) → a ∈ s → κ) (j : (a : κ) → a ∈ t → ι) (hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t) (hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s) (left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a) (right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a) (h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)) : ∑ x ∈ s, f x = ∑ x ∈ t, g x - Finset.card_eq_sum_ones 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} (s : Finset ι) : s.card = ∑ x ∈ s, 1 - Multiset.toFinset_sum_count_eq 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} [DecidableEq ι] (s : Multiset ι) : ∑ a ∈ s.toFinset, Multiset.count a s = s.card - Finset.sum_singleton 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] (f : ι → M) (a : ι) : ∑ x ∈ {a}, f x = f a - Fintype.sum_subsingleton 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} {ι : Type u_7} [Fintype ι] [AddCommMonoid M] [Subsingleton ι] (f : ι → M) (a : ι) : ∑ x, f x = f a - nat_abs_sum_le 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} (s : Finset ι) (f : ι → ℤ) : (∑ i ∈ s, f i).natAbs ≤ ∑ i ∈ s, (f i).natAbs - Finset.sum_range_one 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] (f : ℕ → M) : ∑ k ∈ Finset.range 1, f k = f 0 - List.sum_toFinset_count_eq_length 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} [DecidableEq ι] (l : List ι) : ∑ a ∈ l.toFinset, List.count a l = l.length - Fintype.sum_unique 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} {ι : Type u_7} [Fintype ι] [AddCommMonoid M] [Unique ι] (f : ι → M) : ∑ x, f x = f default - Finset.nsmul_eq_sum_const 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] (b : M) (n : ℕ) : n • b = ∑ _k ∈ Finset.range n, b - Finset.sum_unique_nonempty 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Unique ι] (s : Finset ι) (f : ι → M) (h : s.Nonempty) : ∑ x ∈ s, f x = f default - Finset.card_biUnion_le 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [DecidableEq M] {s : Finset ι} {t : ι → Finset M} : (s.biUnion t).card ≤ ∑ a ∈ s, (t a).card - Finset.sum_const 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] (b : M) : ∑ _x ∈ s, b = s.card • b - IsAddUnit.sum_univ_iff 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [Fintype ι] [AddCommMonoid M] {f : ι → M} : IsAddUnit (∑ a, f a) ↔ ∀ (a : ι), IsAddUnit (f a) - Fintype.sum_Prop 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] (f : Prop → M) : ∑ p, f p = f True + f False - IsAddUnit.sum_iff 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} : IsAddUnit (∑ a ∈ s, f a) ↔ ∀ a ∈ s, IsAddUnit (f a) - Multiset.prod_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} {ι : Type u_5} [CommMonoid M] (f : ι → Multiset M) (s : Finset ι) : (∑ x ∈ s, f x).prod = ∏ x ∈ s, (f x).prod - Multiset.sum_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} {ι : Type u_5} [AddCommMonoid M] (f : ι → Multiset M) (s : Finset ι) : (∑ x ∈ s, f x).sum = ∑ x ∈ s, (f x).sum - Finset.card_disjiUnion 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} (s : Finset ι) (t : ι → Finset M) (h : (↑s).PairwiseDisjoint t) : (s.disjiUnion t h).card = ∑ a ∈ s, (t a).card - Finset.card_eq_sum_card_image 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [DecidableEq M] (f : ι → M) (s : Finset ι) : s.card = ∑ b ∈ Finset.image f s, {a ∈ s | f a = b}.card - Finset.sum_multiset_count 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] [DecidableEq M] (s : Multiset M) : s.sum = ∑ m ∈ s.toFinset, Multiset.count m s • m - Multiset.sum_count_eq_card 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} [DecidableEq ι] {s : Finset ι} {m : Multiset ι} (hms : ∀ a ∈ m, a ∈ s) : ∑ a ∈ s, Multiset.count a m = m.card - Finset.card_biUnion 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [DecidableEq M] {t : ι → Finset M} (h : (↑s).PairwiseDisjoint t) : (s.biUnion t).card = ∑ u ∈ s, (t u).card - Finset.sum_const_nat 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {s : Finset ι} {m : ℕ} {f : ι → ℕ} (h₁ : ∀ x ∈ s, f x = m) : ∑ x ∈ s, f x = s.card * m - Finset.sum_diag 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] (s : Finset ι) (f : ι × ι → M) : ∑ i ∈ s.diag, f i = ∑ i ∈ s, f (i, i) - Finset.eq_of_card_le_one_of_sum_eq 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} (hc : s.card ≤ 1) {f : ι → M} {b : M} (h : ∑ x ∈ s, f x = b) (x : ι) : x ∈ s → f x = b - List.sum_toFinset 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_5} [DecidableEq ι] [AddCommMonoid M] (f : ι → M) {l : List ι} (_hl : l.Nodup) : l.toFinset.sum f = (List.map f l).sum - Finset.sum_congr 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f g : ι → M} (h : s₁ = s₂) : (∀ x ∈ s₂, f x = g x) → s₁.sum f = s₂.sum g - Finset.card_eq_sum_card_fiberwise 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [DecidableEq M] {f : ι → M} {s : Finset ι} {t : Finset M} (H : Set.MapsTo f ↑s ↑t) : s.card = ∑ b ∈ t, {a ∈ s | f a = b}.card - Finset.sum_multiset_map_count 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} [DecidableEq ι] (s : Multiset ι) {M : Type u_5} [AddCommMonoid M] (f : ι → M) : (Multiset.map f s).sum = ∑ m ∈ s.toFinset, Multiset.count m s • f m - Finset.sum_subtype_eq_sum_filter 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] (f : ι → M) {p : ι → Prop} [DecidablePred p] : ∑ x ∈ Finset.subtype p s, f ↑x = ∑ x ∈ {x ∈ s | p x}, f x - Finset.sum_eq_card_nsmul 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} {b : M} (hf : ∀ a ∈ s, f a = b) : ∑ a ∈ s, f a = s.card • b - Finset.sum_erase 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] (s : Finset ι) {f : ι → M} {a : ι} (h : f a = 0) : ∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x - Finset.sum_multiset_count_of_subset 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] [DecidableEq M] (m : Multiset M) (s : Finset M) (hs : m.toFinset ⊆ s) : m.sum = ∑ i ∈ s, Multiset.count i m • i - Multiset.mem_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {a : ι} {s : Finset ι} {m : ι → Multiset ι} : a ∈ ∑ i ∈ s, m i ↔ ∃ i ∈ s, a ∈ m i - Finset.mem_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {f : ι → Multiset M} (s : Finset ι) (b : M) : b ∈ ∑ x ∈ s, f x ↔ ∃ a ∈ s, b ∈ f a - Finset.sum_set_coe 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {f : ι → M} (s : Set ι) [Fintype ↑s] : ∑ i, f ↑i = ∑ i ∈ s.toFinset, f i - Finset.prod_pow_eq_pow_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [CommMonoid M] (s : Finset ι) (f : ι → ℕ) (a : M) : ∏ i ∈ s, a ^ f i = a ^ ∑ i ∈ s, f i - Finset.sum_insert_zero 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] (h : f a = 0) : ∑ x ∈ insert a s, f x = ∑ x ∈ s, f x - Finset.sum_nsmul_assoc 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] (s : Finset ι) (f : ι → ℕ) (a : M) : ∑ i ∈ s, f i • a = (∑ i ∈ s, f i) • a - Finset.sum_range_succ 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] (f : ℕ → M) (n : ℕ) : ∑ x ∈ Finset.range (n + 1), f x = ∑ x ∈ Finset.range n, f x + f n - Finset.sum_range_succ_comm 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] (f : ℕ → M) (n : ℕ) : ∑ x ∈ Finset.range (n + 1), f x = f n + ∑ x ∈ Finset.range n, f x - Finset.sum_subtype_of_mem 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] (f : ι → M) {p : ι → Prop} [DecidablePred p] (h : ∀ x ∈ s, p x) : ∑ x ∈ Finset.subtype p s, f ↑x = ∑ x ∈ s, f x - Finset.eventually_constant_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] {u : ℕ → M} {N : ℕ} (hu : ∀ n ≥ N, u n = 0) {n : ℕ} (hn : N ≤ n) : ∑ k ∈ Finset.range n, u k = ∑ k ∈ Finset.range N, u k - Finset.sum_disjiUnion 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] {f : ι → M} (s : Finset κ) (t : κ → Finset ι) (h : (↑s).PairwiseDisjoint t) : ∑ x ∈ s.disjiUnion t h, f x = ∑ i ∈ s, ∑ x ∈ t i, f x - Finset.sum_fiberwise 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] [DecidableEq κ] [Fintype κ] (s : Finset ι) (g : ι → κ) (f : ι → M) : ∑ j, ∑ i ∈ {i ∈ s | g i = j}, f i = ∑ i ∈ s, f i - Finset.sum_cons 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [AddCommMonoid M] {f : ι → M} (h : a ∉ s) : ∑ x ∈ Finset.cons a s h, f x = f a + ∑ x ∈ s, f x - Finset.sum_eq_zero 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} (h : ∀ x ∈ s, f x = 0) : ∑ x ∈ s, f x = 0 - Finset.sum_extend_by_zero 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] (s : Finset ι) (f : ι → M) : (∑ i ∈ s, if i ∈ s then f i else 0) = ∑ i ∈ s, f i - Finset.sum_fiberwise' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] [DecidableEq κ] [Fintype κ] (s : Finset ι) (g : ι → κ) (f : κ → M) : ∑ j, ∑ i ∈ {i ∈ s | g i = j}, f j = ∑ i ∈ s, f (g i) - Finset.sum_filter 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] (p : ι → Prop) [DecidablePred p] (f : ι → M) : ∑ a ∈ {a ∈ s | p a}, f a = ∑ a ∈ s, if p a then f a else 0 - Finset.sum_finset_coe 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] (f : ι → M) (s : Finset ι) : ∑ i, f ↑i = ∑ i ∈ s, f i - Finset.sum_list_count 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] [DecidableEq M] (s : List M) : s.sum = ∑ m ∈ s.toFinset, List.count m s • m - Finset.sum_pair 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] {a b : ι} (h : a ≠ b) : ∑ x ∈ {a, b}, f x = f a + f b - Finset.sum_subtype 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {p : ι → Prop} {F : Fintype (Subtype p)} (s : Finset ι) (h : ∀ (x : ι), x ∈ s ↔ p x) (f : ι → M) : ∑ a ∈ s, f a = ∑ a, f ↑a - Fintype.sum_subset 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} {ι : Type u_7} [Fintype ι] [AddCommMonoid M] {s : Finset ι} {f : ι → M} (h : ∀ (i : ι), f i ≠ 0 → i ∈ s) : ∑ i ∈ s, f i = ∑ i, f i - Finset.add_sum_erase 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] (s : Finset ι) (f : ι → M) {a : ι} (h : a ∈ s) : f a + ∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x - Finset.sum_biUnion 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] {s : Finset κ} {t : κ → Finset ι} (hs : (↑s).PairwiseDisjoint t) : ∑ x ∈ s.biUnion t, f x = ∑ x ∈ s, ∑ i ∈ t x, f i - Finset.sum_card_fiberwise_eq_card_filter 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_5} [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) : ∑ j ∈ t, {i ∈ s | g i = j}.card = {i ∈ s | g i ∈ t}.card - Finset.sum_erase_add 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] (s : Finset ι) (f : ι → M) {a : ι} (h : a ∈ s) : ∑ x ∈ s.erase a, f x + f a = ∑ x ∈ s, f x - Multiset.toFinset_sum_count_nsmul_eq 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} [DecidableEq ι] (s : Multiset ι) : ∑ a ∈ s.toFinset, Multiset.count a s • {a} = s - Finset.exists_ne_zero_of_sum_ne_zero 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} (h : ∑ x ∈ s, f x ≠ 0) : ∃ a ∈ s, f a ≠ 0 - Finset.sum_eq_single_of_mem 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {f : ι → M} (a : ι) (h : a ∈ s) (h₀ : ∀ b ∈ s, b ≠ a → f b = 0) : ∑ x ∈ s, f x = f a - Finset.sum_flip 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] {n : ℕ} (f : ℕ → M) : ∑ r ∈ Finset.range (n + 1), f (n - r) = ∑ k ∈ Finset.range (n + 1), f k - Finset.sum_attach 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] (s : Finset ι) (f : ι → M) : ∑ x ∈ s.attach, f ↑x = ∑ x ∈ s, f x - Finset.sum_erase_eq_sub 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {G : Type u_3} {s : Finset ι} [AddCommGroup G] [DecidableEq ι] {f : ι → G} {a : ι} (h : a ∈ s) : ∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x - f a - Finset.sum_insert 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] : a ∉ s → ∑ x ∈ insert a s, f x = f a + ∑ x ∈ s, f x - Finset.sum_disjUnion 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f : ι → M} (h : Disjoint s₁ s₂) : ∑ x ∈ s₁.disjUnion s₂ h, f x = ∑ x ∈ s₁, f x + ∑ x ∈ s₂, f x - Finset.sum_eq_zero_iff 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} [Subsingleton (AddUnits M)] : ∑ i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0 - Finset.sum_insert_of_eq_zero_if_not_mem 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] (h : a ∉ s → f a = 0) : ∑ x ∈ insert a s, f x = ∑ x ∈ s, f x - Finset.sum_add_sum_compl 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Fintype ι] [DecidableEq ι] (s : Finset ι) (f : ι → M) : ∑ i ∈ s, f i + ∑ i ∈ sᶜ, f i = ∑ i, f i - Finset.sum_compl_add_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Fintype ι] [DecidableEq ι] (s : Finset ι) (f : ι → M) : ∑ i ∈ sᶜ, f i + ∑ i ∈ s, f i = ∑ i, f i - Finset.sum_list_map_count 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] (l : List ι) (f : ι → M) : (List.map f l).sum = ∑ m ∈ l.toFinset, List.count m l • f m - IsCompl.sum_add_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Fintype ι] {s t : Finset ι} (h : IsCompl s t) (f : ι → M) : ∑ i ∈ s, f i + ∑ i ∈ t, f i = ∑ i, f i - Finset.sum_add_distrib 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f g : ι → M} : ∑ x ∈ s, (f x + g x) = ∑ x ∈ s, f x + ∑ x ∈ s, g x - Finset.sum_filter_ne_zero 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {f : ι → M} (s : Finset ι) [(x : ι) → Decidable (f x ≠ 0)] : ∑ x ∈ {x ∈ s | f x ≠ 0}, f x = ∑ x ∈ s, f x - Finset.sum_filter_of_ne 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} {p : ι → Prop} [DecidablePred p] (hp : ∀ x ∈ s, f x ≠ 0 → p x) : ∑ x ∈ {x ∈ s | p x}, f x = ∑ x ∈ s, f x - Finset.sum_list_count_of_subset 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] [DecidableEq M] (m : List M) (s : Finset M) (hs : m.toFinset ⊆ s) : m.sum = ∑ i ∈ s, List.count i m • i - Finset.sum_comp 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_2} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] [DecidableEq κ] (f : κ → M) (g : ι → κ) : ∑ a ∈ s, f (g a) = ∑ b ∈ Finset.image g s, {a ∈ s | g a = b}.card • f b - Finset.sum_image 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] {s : Finset κ} {g : κ → ι} : (∀ x ∈ s, ∀ y ∈ s, g x = g y → x = y) → ∑ x ∈ Finset.image g s, f x = ∑ x ∈ s, f (g x) - Finset.sum_insert_sub 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {G : Type u_3} {s : Finset ι} {a : ι} [AddCommGroup G] [DecidableEq ι] (ha : a ∉ s) (f : ι → G) : ∑ x ∈ insert a s, f x - f a = ∑ x ∈ s, f x - Finset.sum_range_add 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] (f : ℕ → M) (n m : ℕ) : ∑ x ∈ Finset.range (n + m), f x = ∑ x ∈ Finset.range n, f x + ∑ x ∈ Finset.range m, f (n + x) - Finset.sum_sdiff 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] (h : s₁ ⊆ s₂) : ∑ x ∈ s₂ \ s₁, f x + ∑ x ∈ s₁, f x = ∑ x ∈ s₂, f x - Finset.sum_sumElim 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] (s : Finset ι) (t : Finset κ) (f : ι → M) (g : κ → M) : ∑ x ∈ s.disjSum t, Sum.elim f g x = ∑ x ∈ s, f x + ∑ x ∈ t, g x - Finset.sum_sum_elim 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] (s : Finset ι) (t : Finset κ) (f : ι → M) (g : κ → M) : ∑ x ∈ s.disjSum t, Sum.elim f g x = ∑ x ∈ s, f x + ∑ x ∈ t, g x - Finset.sum_disj_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] (s : Finset ι) (t : Finset κ) (f : ι ⊕ κ → M) : ∑ x ∈ s.disjSum t, f x = ∑ x ∈ s, f (Sum.inl x) + ∑ x ∈ t, f (Sum.inr x) - Finset.sum_eq_fold 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] (s : Finset ι) (f : ι → M) : ∑ i ∈ s, f i = Finset.fold (fun x1 x2 => x1 + x2) 0 f s - Finset.sum_image_of_pairwise_eq_zero 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] {f : κ → ι} {g : ι → M} {I : Finset κ} (hf : (↑I).Pairwise fun i j => f i = f j → g (f i) = 0) : ∑ s ∈ Finset.image f I, g s = ∑ i ∈ I, g (f i) - Finset.sum_range_sub 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{G : Type u_3} [AddCommGroup G] (f : ℕ → G) (n : ℕ) : ∑ i ∈ Finset.range n, (f (i + 1) - f i) = f n - f 0 - Finset.sum_range_sub' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{G : Type u_3} [AddCommGroup G] (f : ℕ → G) (n : ℕ) : ∑ i ∈ Finset.range n, (f i - f (i + 1)) = f 0 - f n - Finset.sum_union 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] (h : Disjoint s₁ s₂) : ∑ x ∈ s₁ ∪ s₂, f x = ∑ x ∈ s₁, f x + ∑ x ∈ s₂, f x - Finset.sum_sum_eq_sum_toLeft_add_sum_toRight 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] (s : Finset (ι ⊕ κ)) (f : ι ⊕ κ → M) : ∑ x ∈ s, f x = ∑ x ∈ s.toLeft, f (Sum.inl x) + ∑ x ∈ s.toRight, f (Sum.inr x) - Finset.sum_range_succ' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] (f : ℕ → M) (n : ℕ) : ∑ k ∈ Finset.range (n + 1), f k = ∑ k ∈ Finset.range n, f (k + 1) + f 0 - Finset.sum_subset 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f : ι → M} (h : s₁ ⊆ s₂) (hf : ∀ x ∈ s₂, x ∉ s₁ → f x = 0) : ∑ x ∈ s₁, f x = ∑ x ∈ s₂, f x - Finset.card_nsmul_add_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} {b : M} : s.card • b + ∑ a ∈ s, f a = ∑ a ∈ s, (b + f a) - Finset.sum_add_card_nsmul 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} {b : M} : ∑ a ∈ s, f a + s.card • b = ∑ a ∈ s, (f a + b) - Finset.sum_fiberwise_of_maps_to 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} [DecidableEq κ] {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : ι → M) : ∑ j ∈ t, ∑ i ∈ {i ∈ s | g i = j}, f i = ∑ i ∈ s, f i - Finset.sum_filter_add_sum_filter_not 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] (s : Finset ι) (p : ι → Prop) [DecidablePred p] [(x : ι) → Decidable ¬p x] (f : ι → M) : ∑ x ∈ {x ∈ s | p x}, f x + ∑ x ∈ {x ∈ s | ¬p x}, f x = ∑ x ∈ s, f x - Finset.sum_filter_not_add_sum_filter 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] (s : Finset ι) (p : ι → Prop) [DecidablePred p] [(x : ι) → Decidable ¬p x] (f : ι → M) : ∑ x ∈ {x ∈ s | ¬p x}, f x + ∑ x ∈ {x ∈ s | p x}, f x = ∑ x ∈ s, f x - Finset.eq_sum_range_sub 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{G : Type u_3} [AddCommGroup G] (f : ℕ → G) (n : ℕ) : f n = f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i) - Finset.sum_coe_sort 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} (s : Finset ι) [AddCommMonoid M] (f : ι → M) : ∑ i, f ↑i = ∑ i ∈ s, f i - Finset.sum_erase_lt_of_pos 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_5} [DecidableEq ι] [AddCommMonoid κ] [LT κ] [AddLeftStrictMono κ] {s : Finset ι} {d : ι} (hd : d ∈ s) {f : ι → κ} (hdf : 0 < f d) : ∑ m ∈ s.erase d, f m < ∑ m ∈ s, f m - Finset.sum_fiberwise_eq_sum_filter 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : ι → M) : ∑ j ∈ t, ∑ i ∈ {i ∈ s | g i = j}, f i = ∑ i ∈ {i ∈ s | g i ∈ t}, f i - Finset.sum_fiberwise_of_maps_to' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} [DecidableEq κ] {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : κ → M) : ∑ j ∈ t, ∑ i ∈ {i ∈ s | g i = j}, f j = ∑ i ∈ s, f (g i) - Finset.sum_range_add_sub_sum_range 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{G : Type u_3} [AddCommGroup G] (f : ℕ → G) (n m : ℕ) : ∑ k ∈ Finset.range (n + m), f k - ∑ k ∈ Finset.range n, f k = ∑ k ∈ Finset.range m, f (n + k) - Finset.sum_sdiff_eq_sub 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {G : Type u_3} {s₁ s₂ : Finset ι} [AddCommGroup G] [DecidableEq ι] {f : ι → G} (h : s₁ ⊆ s₂) : ∑ x ∈ s₂ \ s₁, f x = ∑ x ∈ s₂, f x - ∑ x ∈ s₁, f x - Finset.sum_sdiff_eq_sum_sdiff_iff 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [DecidableEq ι] [AddCancelCommMonoid M] {s t : Finset ι} {f : ι → M} : ∑ i ∈ s \ t, f i = ∑ i ∈ t \ s, f i ↔ ∑ i ∈ s, f i = ∑ i ∈ t, f i - Finset.sum_sdiff_ne_sum_sdiff_iff 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [DecidableEq ι] [AddCancelCommMonoid M] {s t : Finset ι} {f : ι → M} : ∑ i ∈ s \ t, f i ≠ ∑ i ∈ t \ s, f i ↔ ∑ i ∈ s, f i ≠ ∑ i ∈ t, f i - Finset.sum_union_eq_left 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] (hs : ∀ a ∈ s₂, a ∉ s₁ → f a = 0) : ∑ a ∈ s₁ ∪ s₂, f a = ∑ a ∈ s₁, f a - Finset.sum_union_eq_right 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] (hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 0) : ∑ a ∈ s₁ ∪ s₂, f a = ∑ a ∈ s₂, f a - Finset.sum_fiberwise_eq_sum_filter' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : κ → M) : ∑ j ∈ t, ∑ i ∈ {i ∈ s | g i = j}, f j = ∑ i ∈ {i ∈ s | g i ∈ t}, f (g i) - Finset.sum_eq_single 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {f : ι → M} (a : ι) (h₀ : ∀ b ∈ s, b ≠ a → f b = 0) (h₁ : a ∉ s → f a = 0) : ∑ x ∈ s, f x = f a - Finset.sum_image' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] {s : Finset κ} {g : κ → ι} (h : κ → M) (eq : ∀ i ∈ s, f (g i) = ∑ j ∈ {j ∈ s | g j = g i}, h j) : ∑ a ∈ Finset.image g s, f a = ∑ i ∈ s, h i - Finset.sum_range_induction 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] (f s : ℕ → M) (base : s 0 = 0) (step : ∀ (n : ℕ), s (n + 1) = s n + f n) (n : ℕ) : ∑ k ∈ Finset.range n, f k = s n - Fintype.sum_of_injective 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} {κ : Type u_6} {ι : Type u_7} [Fintype ι] [Fintype κ] [AddCommMonoid M] (e : ι → κ) (he : Function.Injective e) (f : ι → M) (g : κ → M) (h' : ∀ i ∉ Set.range e, g i = 0) (h : ∀ (i : ι), f i = g (e i)) : ∑ i, f i = ∑ j, g j - Finset.sum_image_of_disjoint 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] [PartialOrder ι] [OrderBot ι] {f : κ → ι} {g : ι → M} (hg_bot : g ⊥ = 0) {I : Finset κ} (hf_disj : (↑I).PairwiseDisjoint f) : ∑ s ∈ Finset.image f I, g s = ∑ i ∈ I, g (f i) - Fintype.sum_fiberwise' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} {κ : Type u_6} {ι : Type u_7} [Fintype ι] [Fintype κ] [AddCommMonoid M] [DecidableEq κ] (g : ι → κ) (f : κ → M) : ∑ j, ∑ _i, f j = ∑ i, f (g i) - Finset.sum_cancels_of_partition_cancels 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} (R : Setoid ι) [DecidableRel ⇑R] (h : ∀ x ∈ s, ∑ a ∈ {a ∈ s | R a x}, f a = 0) : ∑ x ∈ s, f x = 0 - Finset.sum_filter_of_pairwise_eq_zero 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] {f : κ → ι} {g : ι → M} {n : κ} {I : Finset κ} (hn : n ∈ I) (hf : (↑I).Pairwise fun i j => f i = f j → g (f i) = 0) : ∑ j ∈ {j ∈ I | f j = f n}, g (f j) = g (f n) - Finset.eq_sum_range_sub' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{G : Type u_3} [AddCommGroup G] (f : ℕ → G) (n : ℕ) : f n = ∑ i ∈ Finset.range (n + 1), if i = 0 then f 0 else f i - f (i - 1) - Finset.eq_zero_of_sum_eq_zero 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {f : ι → M} {a : ι} (hp : ∑ x ∈ s, f x = 0) (h1 : ∀ x ∈ s, x ≠ a → f x = 0) (x : ι) : x ∈ s → f x = 0 - Finset.sum_partition 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} (R : Setoid ι) [DecidableRel ⇑R] : ∑ x ∈ s, f x = ∑ xbar ∈ Finset.image (Quotient.mk R) s, ∑ y ∈ {y ∈ s | ⟦y⟧ = xbar}, f y - Finset.sum_subset_zero_on_sdiff 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f g : ι → M} [DecidableEq ι] (h : s₁ ⊆ s₂) (hg : ∀ x ∈ s₂ \ s₁, g x = 0) (hfg : ∀ x ∈ s₁, f x = g x) : ∑ i ∈ s₁, f i = ∑ i ∈ s₂, g i - Finset.sum_union_inter 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] : ∑ x ∈ s₁ ∪ s₂, f x + ∑ x ∈ s₁ ∩ s₂, f x = ∑ x ∈ s₁, f x + ∑ x ∈ s₂, f x - Fintype.sum_fiberwise 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} {κ : Type u_6} {ι : Type u_7} [Fintype ι] [Fintype κ] [AddCommMonoid M] [DecidableEq κ] (g : ι → κ) (f : ι → M) : ∑ j, ∑ i, f ↑i = ∑ i, f i - Finset.sum_eq_add_of_mem 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {f : ι → M} (a b : ι) (ha : a ∈ s) (hb : b ∈ s) (hn : a ≠ b) (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 0) : ∑ x ∈ s, f x = f a + f b - Finset.sum_sdiff_sub_sum_sdiff 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {G : Type u_3} {s₁ s₂ : Finset ι} [AddCommGroup G] [DecidableEq ι] {f : ι → G} : ∑ x ∈ s₂ \ s₁, f x - ∑ x ∈ s₁ \ s₂, f x = ∑ x ∈ s₂, f x - ∑ x ∈ s₁, f x - Finset.sum_subtype_map_embedding 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {p : ι → Prop} {s : Finset { x // p x }} {f : { x // p x } → M} {g : ι → M} (h : ∀ x ∈ s, g ↑x = f x) : ∑ x ∈ Finset.map (Function.Embedding.subtype fun x => p x) s, g x = ∑ x ∈ s, f x - Finset.sum_add_eq_sum_add_of_exists 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {f : ι → M} {b₁ b₂ : M} (a : ι) (ha : a ∈ s) (h : f a + b₁ = f a + b₂) : ∑ a ∈ s, f a + b₁ = ∑ a ∈ s, f a + b₂ - Finset.sum_ninvolution 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} (g : ι → ι) (hg₁ : ∀ (a : ι), f a + f (g a) = 0) (hg₂ : ∀ (a : ι), f a ≠ 0 → g a ≠ a) (g_mem : ∀ (a : ι), g a ∈ s) (hg₃ : ∀ (a : ι), g (g a) = a) : ∑ x ∈ s, f x = 0 - Finset.sum_of_injOn 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (e : ι → κ) (he : Set.InjOn e ↑s) (hest : Set.MapsTo e ↑s ↑t) (h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 0) (h : ∀ i ∈ s, f i = g (e i)) : ∑ i ∈ s, f i = ∑ j ∈ t, g j - Fintype.sum_subtype_add_sum_subtype 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} {ι : Type u_7} [Fintype ι] [AddCommMonoid M] (p : ι → Prop) (f : ι → M) [DecidablePred p] : ∑ i, f ↑i + ∑ i, f ↑i = ∑ i, f i - Finset.sum_eq_sum_extend 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] (f : { x // x ∈ s } → M) : ∑ x, f x = ∑ x ∈ s, Function.extend Subtype.val f 0 x - Finset.sum_congr_set 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Fintype ι] (s : Set ι) [DecidablePred fun x => x ∈ s] (f : ι → M) (g : ↑s → M) (w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩) (w' : ∀ x ∉ s, f x = 0) : ∑ i, f i = ∑ i, g i - Finset.sum_congr_of_eq_on_inter 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_5} {M : Type u_6} {s₁ s₂ : Finset ι} {f g : ι → M} [AddCommMonoid M] (h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 0) (h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 0) (h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a) : ∑ a ∈ s₁, f a = ∑ a ∈ s₂, g a - Finset.sum_filter_xor 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} (p q : ι → Prop) [DecidablePred p] [DecidablePred q] : ∑ x ∈ {x ∈ s | Xor' (p x) (q x)}, f x = ∑ x ∈ {x ∈ s | p x ∧ ¬q x}, f x + ∑ x ∈ {x ∈ s | q x ∧ ¬p x}, f x - Finset.sum_range_tsub 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] [PartialOrder M] [Sub M] [OrderedSub M] [AddLeftMono M] [AddLeftReflectLE M] [ExistsAddOfLE M] {f : ℕ → M} (h : Monotone f) (n : ℕ) : ∑ i ∈ Finset.range n, (f (i + 1) - f i) = f n - f 0 - Finset.sum_eq_add 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {f : ι → M} (a b : ι) (hn : a ≠ b) (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 0) (ha : a ∉ s → f a = 0) (hb : b ∉ s → f b = 0) : ∑ x ∈ s, f x = f a + f b - Finset.sum_tsub_distrib 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [Sub M] [OrderedSub M] [AddLeftMono M] [AddLeftReflectLE M] [ExistsAddOfLE M] (s : Finset ι) {f g : ι → M} (hfg : ∀ x ∈ s, g x ≤ f x) : ∑ x ∈ s, (f x - g x) = ∑ x ∈ s, f x - ∑ x ∈ s, g x - Finset.sum_add_sum_comm 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] (f g h i : ι → M) : ∑ a ∈ s, (f a + g a) + ∑ a ∈ s, (h a + i a) = ∑ a ∈ s, (f a + h a) + ∑ a ∈ s, (g a + i a) - Finset.sum_involution 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} (g : (a : ι) → a ∈ s → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ s), f a + f (g a ha) = 0) (hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 0 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s) (hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a) : ∑ x ∈ s, f x = 0
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. You can also try the
#loogle command from LeanSearchClient,
the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"somewhere in their lemma name.By subexpression:
🔍_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
🔍Real.sqrt ?a * Real.sqrt ?aIf the pattern has parameters, they are matched in any order. Both of these will find
List.map:
🔍(?a -> ?b) -> List ?a -> List ?b
🔍List ?a -> (?a -> ?b) -> List ?bBy main conclusion:
🔍|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all→and∀) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍|- _ < _ → tsum _ < tsum _
will findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin
and tsum, have "two" as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _ (if
there were any such lemmas). Metavariables (?a) are
assigned independently in each filter.
The #lucky button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.
This is Loogle revision b340a5b serving mathlib revision 846a90c