Loogle!

Result

Found 3099 declarations mentioning Finset.sum. Of these, only the first 200 are shown.

Finset.sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (f : ι → M) : M
Finset.sum_val 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{M : Type u_3} [AddCommMonoid M] (s : Finset M) : s.val.sum = s.sum id
Finset.sum.eq_1 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (f : ι → M) : s.sum f = (Multiset.map f s.val).sum
Finset.sum_multiset_singleton 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} (s : Finset ι) : ∑ a ∈ s, {a} = s.val
Finset.sum_eq_multiset_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (f : ι → M) : ∑ x ∈ s, f x = (Multiset.map f s.val).sum
Finset.sum_map_val 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (f : ι → M) : (Multiset.map f s.val).sum = ∑ a ∈ s, f a
Finset.sum_mk 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Multiset ι) (hs : s.Nodup) (f : ι → M) : { val := s, nodup := hs }.sum f = (Multiset.map f s).sum
Finset.sum_empty' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] : ∅.sum = fun x => 0
Finset.sum_empty 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} {f : ι → M} [AddCommMonoid M] : ∑ x ∈ ∅, f x = 0
Finset.sum_of_isEmpty 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} {f : ι → M} [AddCommMonoid M] [IsEmpty ι] (s : Finset ι) : ∑ i ∈ s, f i = 0
Finset.sum_range_zero 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{M : Type u_3} [AddCommMonoid M] (f : ℕ → M) : ∑ k ∈ Finset.range 0, f k = 0
Finset.nonempty_of_sum_ne_zero 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} {s : Finset ι} {f : ι → M} [AddCommMonoid M] (h : ∑ x ∈ s, f x ≠ 0) : s.Nonempty
Finset.sum_toList 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{M : Type u_7} [AddCommMonoid M] (s : Finset M) : s.toList.sum = ∑ x ∈ s, x
Finset.op_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] {s : Finset ι} (f : ι → M) : MulOpposite.op (∑ x ∈ s, f x) = ∑ x ∈ s, MulOpposite.op (f x)
Finset.unop_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] {s : Finset ι} (f : ι → Mᵐᵒᵖ) : MulOpposite.unop (∑ x ∈ s, f x) = ∑ x ∈ s, MulOpposite.unop (f x)
Fintype.sum_empty 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} [Fintype ι] [AddCommMonoid M] [IsEmpty ι] (f : ι → M) : ∑ x, f x = 0
Multiset.card_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {α : Type u_6} (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_1} {M : Type u_3} {s : Finset ι} [AddCommMonoid M] : ∑ _x ∈ s, 0 = 0
Finset.sum_map_toList 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (f : ι → M) : (List.map f s.toList).sum = s.sum f
Finset.sum_to_list 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (f : ι → M) : (List.map f s.toList).sum = s.sum f
Function.Bijective.sum_comp 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [AddCommMonoid M] {e : ι → κ} (he : Function.Bijective e) (g : κ → M) : ∑ i, g (e i) = ∑ i, g i
Multiset.count_sum' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {α : Type u_6} [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_1} [DecidableEq ι] (p : ι → Prop) [DecidablePred p] (l : List ι) : ∑ x ∈ l.toFinset with 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_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (e : ι ↪ κ) : (Finset.map e s).sum = fun f => ∑ x ∈ s, f (e x)
Finset.sum_map 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (e : ι ↪ κ) (f : κ → M) : ∑ x ∈ Finset.map e s, f x = ∑ x ∈ s, f (e x)
Finset.sum_int_mod 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} (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_1} (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_1} {α : 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_1} {α : 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_1} {M : Type u_3} [AddCommMonoid M] (p : Prop) [Decidable p] (s t : Finset ι) (f : ι → M) : ∑ 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_1} {M : Type u_3} [AddCommMonoid M] (p : Prop) [Decidable p] (s : Finset ι) (f g : ι → M) : (∑ 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_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [AddCommMonoid M] (e : ι → κ) (he : Function.Bijective e) (f : ι → M) (g : κ → M) (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_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [AddCommMonoid M] (e : ι → κ) (he : Function.Bijective e) (f : ι → M) (g : κ → M) (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_1} {G : Type u_5} {s : Finset ι} [SubtractionCommMonoid G] (f : ι → G) : ∑ x ∈ s, -f x = -∑ x ∈ s, f x
Equiv.sum_comp 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [AddCommMonoid M] (e : ι ≃ κ) (g : κ → M) : ∑ i, g (e i) = ∑ i, g i
Finset.sum_nsmul 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (n : ℕ) (f : ι → M) : ∑ x ∈ s, n • f x = n • ∑ x ∈ s, f x
Finset.sum_induction_nonempty 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {s : Finset ι} {M : Type u_7} [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)
Finset.ite_sum_zero 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (p : Prop) [Decidable p] (s : Finset ι) (f : ι → M) : (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_1} {M : Type u_3} [AddCommMonoid M] (p : Prop) [Decidable p] (s : Finset ι) (f : ι → M) : (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_1} {G : Type u_5} [SubtractionCommMonoid G] (f : ι → G) (s : Finset ι) (n : ℤ) : ∑ a ∈ s, n • f a = n • ∑ a ∈ s, f a
Finset.sum_dite_irrel 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (p : Prop) [Decidable p] (s : Finset ι) (f : p → ι → M) (g : ¬p → ι → M) : (∑ 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
Fintype.sum_equiv 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [AddCommMonoid M] (e : ι ≃ κ) (f : ι → M) (g : κ → M) (h : ∀ (x : ι), f x = g (e x)) : ∑ x, f x = ∑ x, g x
map_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] {G : Type u_7} [FunLike G M N] [AddMonoidHomClass G M N] (g : G) (f : ι → M) (s : Finset ι) : g (∑ x ∈ s, f x) = ∑ x ∈ s, g (f x)
Finset.sum_induction 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {s : Finset ι} {M : Type u_7} [AddCommMonoid M] (f : ι → M) (p : M → Prop) (hom : ∀ (a b : M), p a → p b → p (a + b)) (addUnit : 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_1} {G : Type u_5} {s : Finset ι} [SubtractionCommMonoid G] (f g : ι → G) : ∑ 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_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (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_1} {M : Type u_3} [AddCommMonoid M] (σ : Equiv.Perm ι) (s : Finset ι) (f : ι → M) (hs : {a | σ a ≠ a} ⊆ ↑s) : ∑ x ∈ s, f (σ x) = ∑ x ∈ s, f x
ofAdd_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (f : ι → M) : Multiplicative.ofAdd (∑ i ∈ s, f i) = ∏ i ∈ s, Multiplicative.ofAdd (f i)
ofMul_prod 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} [CommMonoid M] (s : Finset ι) (f : ι → M) : Additive.ofMul (∏ i ∈ s, f i) = ∑ i ∈ s, Additive.ofMul (f i)
toAdd_prod 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (f : ι → Multiplicative M) : Multiplicative.toAdd (∏ i ∈ s, f i) = ∑ i ∈ s, Multiplicative.toAdd (f i)
toMul_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} [CommMonoid M] (s : Finset ι) (f : ι → Additive M) : Additive.toMul (∑ i ∈ s, f i) = ∏ i ∈ s, Additive.toMul (f i)
Finset.sum_nbij 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (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} {M : Type u_3} [AddCommMonoid M] [Fintype ι] (f : { i // i ∈ Finset.univ } → M) : ∑ i ∈ Finset.univ.attach, f i = ∑ i, f ⟨i, ⋯⟩
Finset.sum_coe_sort_eq_attach 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} (s : Finset ι) [AddCommMonoid M] (f : { x // x ∈ s } → M) : ∑ i, f i = ∑ i ∈ s.attach, f i
Equiv.Perm.sum_comp' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (σ : Equiv.Perm ι) (s : Finset ι) (f : ι → ι → M) (hs : {a | σ a ≠ a} ⊆ ↑s) : ∑ x ∈ s, f (σ x) x = ∑ x ∈ s, f x ((Equiv.symm σ) x)
Finset.sum_hom_rel 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] {r : M → N → Prop} {f : ι → M} {g : ι → N} {s : Finset ι} (h₁ : r 0 0) (h₂ : ∀ (a : ι) (b : M) (c : N), r b c → r (f a + b) (g a + c)) : r (∑ x ∈ s, f x) (∑ x ∈ s, g x)
Finset.sum_equiv 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (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_mem_multiset 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [DecidableEq ι] (m : Multiset ι) (f : { x // x ∈ m } → M) (g : ι → M) (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_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (i : ι → κ) (j : κ → ι) (hi : ∀ a ∈ s, i a ∈ t) (hj : ∀ a ∈ t, j a ∈ s) (left_neg : ∀ a ∈ s, j (i a) = a) (right_neg : ∀ 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} {M : Type u_3} [AddCommMonoid M] [DecidableEq ι] {s : Finset ι} (f : ι → M) (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_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (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_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (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_neg : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a) (right_neg : ∀ (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
Finset.sum_singleton' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] (a : ι) : {a}.sum = fun f => f a
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.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 : κ → ι} : Set.InjOn g ↑s → ∑ x ∈ Finset.image g s, f x = ∑ x ∈ s, f (g x)
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 ∈ s with 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_cons' 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [AddCommMonoid M] (h : a ∉ s) : (Finset.cons a s h).sum = fun f => f a + ∑ x ∈ s, f x
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 ∈ s with 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 ∈ s with 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 ∈ s with 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] [DecidableEq ι] (h : a ∉ s) : (insert a s).sum = fun f => f a + ∑ x ∈ s, f x
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_notMem 📋 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_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 ∈ s with 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 ∈ s with 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_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_disjSum 📋 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_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 ∈ s with 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 ∈ s with p x, f x + ∑ x ∈ s with ¬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 ∈ s with ¬p x, f x + ∑ x ∈ s with 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 ∈ s with g i = j, f i = ∑ i ∈ s with 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 ∈ s with 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 ∈ s with g i = j, f j = ∑ i ∈ s with 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 ∈ s with g j = g i, h j) : ∑ a ∈ Finset.image g s, f a = ∑ i ∈ s, h i
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_eq_ite 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] {s : Finset ι} {f : ι → M} (a : ι) (h₀ : ∀ b ∈ s, b ≠ a → f b = 0) : ∑ x ∈ s, f x = if a ∈ s then f a else 0
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)
Finset.sum_range_induction 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
{M : Type u_4} [AddCommMonoid M] (f s : ℕ → M) (base : s 0 = 0) (n : ℕ) (step : ∀ k < n, s (k + 1) = s k + f k) : ∑ k ∈ Finset.range n, f k = s n
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 ∈ s with 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 ∈ I with 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 ∈ s with ⟦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

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 ?a

If 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 ?b
By 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 find tsum_lt_tsum even though the hypothesis f i < g i is 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 06e7f72 serving mathlib revision ce21d9f