Loogle!

Result

Found 61 declarations whose name contains "multiset_sum".

map_multiset_sum 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
{F : Type u_1} {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (s : Multiset M) : f s.sum = (Multiset.map (⇑f) s).sum
AddMonoidHom.map_multiset_sum 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
{M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] (f : M →+ N) (s : Multiset M) : f s.sum = (Multiset.map (⇑f) s).sum
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
toAdd_multiset_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{M : Type u_3} [AddCommMonoid M] (s : Multiset (Multiplicative M)) : Multiplicative.toAdd s.prod = (Multiset.map (⇑Multiplicative.toAdd) s).sum
toMul_multiset_sum 📋 Mathlib.Algebra.BigOperators.Group.Finset.Defs
{M : Type u_3} [CommMonoid M] (s : Multiset (Additive M)) : Additive.toMul s.sum = (Multiset.map (⇑Additive.toMul) s).prod
multiset_sum_mem 📋 Mathlib.Algebra.Group.Submonoid.BigOperators
{B : Type u_3} {S : B} {M : Type u_4} [AddCommMonoid M] [SetLike B M] [AddSubmonoidClass B M] (m : Multiset M) (hm : ∀ a ∈ m, a ∈ S) : m.sum ∈ S
AddSubmonoid.multiset_sum_mem 📋 Mathlib.Algebra.Group.Submonoid.BigOperators
{M : Type u_4} [AddCommMonoid M] (S : AddSubmonoid M) (m : Multiset M) (hm : ∀ a ∈ m, a ∈ S) : m.sum ∈ S
AddSubmonoidClass.coe_multiset_sum 📋 Mathlib.Algebra.Group.Submonoid.BigOperators
{B : Type u_3} {S : B} {M : Type u_4} [AddCommMonoid M] [SetLike B M] [AddSubmonoidClass B M] (m : Multiset ↥S) : ↑m.sum = (Multiset.map Subtype.val m).sum
AddSubmonoid.coe_multiset_sum 📋 Mathlib.Algebra.Group.Submonoid.BigOperators
{M : Type u_4} [AddCommMonoid M] (S : AddSubmonoid M) (m : Multiset ↥S) : ↑m.sum = (Multiset.map Subtype.val m).sum
Subsemiring.multiset_sum_mem 📋 Mathlib.Algebra.Ring.Subsemiring.Basic
{R : Type u} [NonAssocSemiring R] (s : Subsemiring R) (m : Multiset R) : (∀ a ∈ m, a ∈ s) → m.sum ∈ s
Subring.multiset_sum_mem 📋 Mathlib.Algebra.Ring.Subring.Basic
{R : Type u_1} [Ring R] (s : Subring R) (m : Multiset R) : (∀ a ∈ m, a ∈ s) → m.sum ∈ s
Pi.multiset_sum_apply 📋 Mathlib.Algebra.BigOperators.Pi
{α : Type u_7} {M : α → Type u_8} [(a : α) → AddCommMonoid (M a)] (a : α) (s : Multiset ((a : α) → M a)) : s.sum a = (Multiset.map (fun f => f a) s).sum
Commute.multiset_sum_left 📋 Mathlib.Algebra.BigOperators.Ring.Multiset
{R : Type u_4} [NonUnitalNonAssocSemiring R] (s : Multiset R) (b : R) (h : ∀ a ∈ s, Commute a b) : Commute s.sum b
Commute.multiset_sum_right 📋 Mathlib.Algebra.BigOperators.Ring.Multiset
{R : Type u_4} [NonUnitalNonAssocSemiring R] (s : Multiset R) (a : R) (h : ∀ b ∈ s, Commute a b) : Commute a s.sum
Nat.cast_multiset_sum 📋 Mathlib.Algebra.BigOperators.Ring.Finset
{R : Type u_4} [AddCommMonoidWithOne R] (s : Multiset ℕ) : ↑s.sum = (Multiset.map Nat.cast s).sum
Int.cast_multiset_sum 📋 Mathlib.Algebra.BigOperators.Ring.Finset
{R : Type u_4} [AddCommGroupWithOne R] (s : Multiset ℤ) : ↑s.sum = (Multiset.map Int.cast s).sum
Finsupp.multiset_sum_sum 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
{α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {f : α →₀ M} {h : α → M → Multiset N} : (f.sum h).sum = f.sum fun a b => (h a b).sum
Finsupp.single_multiset_sum 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
{α : Type u_1} {M : Type u_8} [AddCommMonoid M] (s : Multiset M) (a : α) : (fun₀ | a => s.sum) = (Multiset.map (Finsupp.single a) s).sum
Finsupp.multiset_sum_sum_index 📋 Mathlib.Algebra.BigOperators.Finsupp.Basic
{α : Type u_1} {M : Type u_8} {N : Type u_10} [AddCommMonoid M] [AddCommMonoid N] (f : Multiset (α →₀ M)) (h : α → M → N) (h₀ : ∀ (a : α), h a 0 = 0) (h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) : f.sum.sum h = (Multiset.map (fun g => g.sum h) f).sum
Rat.cast_multiset_sum 📋 Mathlib.Data.Rat.BigOperators
{α : Type u_2} [DivisionRing α] [CharZero α] (s : Multiset ℚ) : ↑s.sum = (Multiset.map Rat.cast s).sum
Finsupp.mem_support_multiset_sum 📋 Mathlib.Data.Finsupp.Basic
{α : Type u_1} {M : Type u_5} [AddCommMonoid M] {s : Multiset (α →₀ M)} (a : α) : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support
Finsupp.mapRange_multiset_sum 📋 Mathlib.Data.Finsupp.Basic
{α : Type u_1} {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] {F : Type u_12} [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (m : Multiset (α →₀ M)) : Finsupp.mapRange ⇑f ⋯ m.sum = (Multiset.map (fun x => Finsupp.mapRange ⇑f ⋯ x) m).sum
AddSubgroup.multiset_sum_mem 📋 Mathlib.Algebra.Group.Subgroup.Finite
{G : Type u_3} [AddCommGroup G] (K : AddSubgroup G) (g : Multiset G) : (∀ a ∈ g, a ∈ K) → g.sum ∈ K
AddSubgroup.val_multiset_sum 📋 Mathlib.Algebra.Group.Subgroup.Finite
{G : Type u_3} [AddCommGroup G] (H : AddSubgroup G) (m : Multiset ↥H) : ↑m.sum = (Multiset.map Subtype.val m).sum
Ideal.pow_multiset_sum_mem_span_pow 📋 Mathlib.RingTheory.Ideal.Basic
{α : Type u_2} [CommSemiring α] [DecidableEq α] (s : Multiset α) (n : ℕ) : s.sum ^ (s.card * n + 1) ∈ Ideal.span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
Set.multiset_sum_singleton 📋 Mathlib.Algebra.Group.Pointwise.Set.BigOperators
{M : Type u_5} [AddCommMonoid M] (s : Multiset M) : (Multiset.map (fun i => {i}) s).sum = {s.sum}
Set.multiset_sum_mem_multiset_sum 📋 Mathlib.Algebra.Group.Pointwise.Set.BigOperators
{ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (t : Multiset ι) (f : ι → Set α) (g : ι → α) (hg : ∀ i ∈ t, g i ∈ f i) : (Multiset.map g t).sum ∈ (Multiset.map f t).sum
Set.multiset_sum_subset_multiset_sum 📋 Mathlib.Algebra.Group.Pointwise.Set.BigOperators
{ι : Type u_1} {α : Type u_2} [AddCommMonoid α] (t : Multiset ι) (f₁ f₂ : ι → Set α) (hf : ∀ i ∈ t, f₁ i ⊆ f₂ i) : (Multiset.map f₁ t).sum ⊆ (Multiset.map f₂ t).sum
Set.image_multiset_sum 📋 Mathlib.Algebra.Group.Pointwise.Set.BigOperators
{α : Type u_2} {β : Type u_3} {F : Type u_4} [FunLike F α β] [AddCommMonoid α] [AddCommMonoid β] [AddMonoidHomClass F α β] (f : F) (m : Multiset (Set α)) : ⇑f '' m.sum = (Multiset.map (fun s => ⇑f '' s) m).sum
RingEquiv.map_multiset_sum 📋 Mathlib.Algebra.BigOperators.RingEquiv
{R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R ≃+* S) (s : Multiset R) : f s.sum = (Multiset.map (⇑f) s).sum
Matrix.diag_multiset_sum 📋 Mathlib.Data.Matrix.Basic
{n : Type u_3} {α : Type u_11} [AddCommMonoid α] (s : Multiset (Matrix n n α)) : s.sum.diag = (Multiset.map Matrix.diag s).sum
Matrix.transpose_multiset_sum 📋 Mathlib.Data.Matrix.Basic
{m : Type u_2} {n : Type u_3} {α : Type u_11} [AddCommMonoid α] (s : Multiset (Matrix m n α)) : s.sum.transpose = (Multiset.map Matrix.transpose s).sum
Finsupp.toMultiset_sum_single 📋 Mathlib.Data.Finsupp.Multiset
{ι : Type u_3} (s : Finset ι) (n : ℕ) : Finsupp.toMultiset (∑ i ∈ s, fun₀ | i => n) = n • s.val
Finsupp.toMultiset_sum 📋 Mathlib.Data.Finsupp.Multiset
{α : Type u_1} {ι : Type u_3} {f : ι → α →₀ ℕ} (s : Finset ι) : Finsupp.toMultiset (∑ i ∈ s, f i) = ∑ i ∈ s, Finsupp.toMultiset (f i)
NonUnitalSubring.multiset_sum_mem 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
{R : Type u_1} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) (m : Multiset R) : (∀ a ∈ m, a ∈ s) → m.sum ∈ s
Subalgebra.multiset_sum_mem 📋 Mathlib.Algebra.Algebra.Subalgebra.Basic
{R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {m : Multiset A} (h : ∀ x ∈ m, x ∈ S) : m.sum ∈ S
Matrix.conjTranspose_multiset_sum 📋 Mathlib.LinearAlgebra.Matrix.ConjTranspose
{m : Type u_2} {n : Type u_3} {α : Type v} [AddCommMonoid α] [StarAddMonoid α] (s : Multiset (Matrix m n α)) : s.sum.conjTranspose = (Multiset.map Matrix.conjTranspose s).sum
Polynomial.eval₂_multiset_sum 📋 Mathlib.Algebra.Polynomial.Eval.Defs
{R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) (s : Multiset (Polynomial R)) (x : S) : Polynomial.eval₂ f x s.sum = (Multiset.map (Polynomial.eval₂ f x) s).sum
Polynomial.natDegree_multiset_sum_le 📋 Mathlib.Algebra.Polynomial.BigOperators
{S : Type u_1} [Semiring S] (l : Multiset (Polynomial S)) : l.sum.natDegree ≤ Multiset.foldr max 0 (Multiset.map Polynomial.natDegree l)
multiset_sum_pow_char 📋 Mathlib.Algebra.CharP.Lemmas
{R : Type u_3} [CommSemiring R] (p : ℕ) [ExpChar R p] (s : Multiset R) : s.sum ^ p = (Multiset.map (fun x => x ^ p) s).sum
multiset_sum_pow_char_pow 📋 Mathlib.Algebra.CharP.Lemmas
{R : Type u_3} [CommSemiring R] (p n : ℕ) [ExpChar R p] (s : Multiset R) : s.sum ^ p ^ n = (Multiset.map (fun x => x ^ p ^ n) s).sum
Subfield.multiset_sum_mem 📋 Mathlib.Algebra.Field.Subfield.Basic
{K : Type u} [DivisionRing K] (s : Subfield K) (m : Multiset K) : (∀ a ∈ m, a ∈ s) → m.sum ∈ s
Localization.mk_multiset_sum 📋 Mathlib.RingTheory.Localization.Defs
{R : Type u_1} [CommSemiring R] {M : Submonoid R} (l : Multiset R) (b : ↥M) : Localization.mk l.sum b = (Multiset.map (fun a => Localization.mk a b) l).sum
continuous_multiset_sum 📋 Mathlib.Topology.Algebra.Monoid
{ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} (s : Multiset ι) : (∀ i ∈ s, Continuous (f i)) → Continuous fun a => (Multiset.map (fun i => f i a) s).sum
continuousOn_multiset_sum 📋 Mathlib.Topology.Algebra.Monoid
{ι : Type u_1} {M : Type u_3} {X : Type u_5} [TopologicalSpace X] [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} (s : Multiset ι) {t : Set X} : (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => (Multiset.map (fun i => f i a) s).sum) t
tendsto_multiset_sum 📋 Mathlib.Topology.Algebra.Monoid
{ι : Type u_1} {α : Type u_2} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Multiset ι) : (∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun b => (Multiset.map (fun c => f c b) s).sum) x (nhds (Multiset.map a s).sum)
NNReal.coe_multiset_sum 📋 Mathlib.Data.NNReal.Basic
(s : Multiset NNReal) : ↑s.sum = (Multiset.map NNReal.toReal s).sum
CharTwo.multiset_sum_sq 📋 Mathlib.Algebra.CharP.Two
{R : Type u_1} [CommSemiring R] [CharP R 2] (l : Multiset R) : l.sum ^ 2 = (Multiset.map (fun x => x ^ 2) l).sum
CharTwo.multiset_sum_mul_self 📋 Mathlib.Algebra.CharP.Two
{R : Type u_1} [CommSemiring R] [CharP R 2] (l : Multiset R) : l.sum * l.sum = (Multiset.map (fun x => x * x) l).sum
Matrix.trace_multiset_sum 📋 Mathlib.LinearAlgebra.Matrix.Trace
{n : Type u_3} {R : Type u_6} [Fintype n] [AddCommMonoid R] (s : Multiset (Matrix n n R)) : s.sum.trace = (Multiset.map Matrix.trace s).sum
LinearMap.BilinMap.toQuadraticMap_multiset_sum 📋 Mathlib.LinearAlgebra.QuadraticForm.Basic
{R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (B : Multiset (LinearMap.BilinMap R M N)) : B.sum.toQuadraticMap = (Multiset.map LinearMap.BilinMap.toQuadraticMap B).sum
IsIntegral.multiset_sum 📋 Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
{R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {s : Multiset A} (h : ∀ x ∈ s, IsIntegral R x) : IsIntegral R s.sum
IntermediateField.multiset_sum_mem 📋 Mathlib.FieldTheory.IntermediateField.Basic
{K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (m : Multiset L) : (∀ a ∈ m, a ∈ S) → m.sum ∈ S
norm_multiset_sum_le 📋 Mathlib.Analysis.Normed.Group.Basic
{E : Type u_9} [SeminormedAddCommGroup E] (m : Multiset E) : ‖m.sum‖ ≤ (Multiset.map (fun x => ‖x‖) m).sum
nnnorm_multiset_sum_le 📋 Mathlib.Analysis.Normed.Group.Basic
{E : Type u_5} [SeminormedAddCommGroup E] (m : Multiset E) : ‖m.sum‖₊ ≤ (Multiset.map (fun x => ‖x‖₊) m).sum
Real.exp_multiset_sum 📋 Mathlib.Analysis.Complex.Exponential
(s : Multiset ℝ) : Real.exp s.sum = (Multiset.map Real.exp s).prod
Complex.exp_multiset_sum 📋 Mathlib.Analysis.Complex.Exponential
(s : Multiset ℂ) : Complex.exp s.sum = (Multiset.map Complex.exp s).prod
convex_multiset_sum 📋 Mathlib.Analysis.Convex.Basic
{𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Module 𝕜 E] {s : Multiset (Set E)} (h : ∀ i ∈ s, Convex 𝕜 i) : Convex 𝕜 s.sum
convexHull_multiset_sum 📋 Mathlib.Analysis.Convex.Combination
{R : Type u_1} {E : Type u_3} [Field R] [AddCommGroup E] [Module R E] [LinearOrder R] [IsStrictOrderedRing R] (s : Multiset (Set E)) : (convexHull R) s.sum = (Multiset.map (⇑(convexHull R)) s).sum
IsUltrametricDist.exists_norm_multiset_sum_le 📋 Mathlib.Analysis.Normed.Group.Ultra
{M : Type u_1} {ι : Type u_2} [SeminormedAddCommGroup M] [IsUltrametricDist M] (s : Multiset ι) [Nonempty ι] {f : ι → M} : ∃ i, (s ≠ 0 → i ∈ s) ∧ ‖(Multiset.map f s).sum‖ ≤ ‖f i‖
AddCon.multiset_sum 📋 Mathlib.GroupTheory.Congruence.BigOperators
{ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (c : AddCon M) {s : Multiset ι} {f g : ι → M} (h : ∀ x ∈ s, c (f x) (g x)) : c (Multiset.map f s).sum (Multiset.map g s).sum

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 6ff4759 serving mathlib revision 519f454