Big operators for finsupps

This file contains theorems relevant to big operators in finitely supported functions.

Declarations about Finsupp.sum and Finsupp.prod

In most of this section, the domain β is assumed to be an AddMonoid.

def Finsupp.prod {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] (f : α →₀ M) (g : α → M → N) : N

prod f g is the product of g a (f a) over the support of f.

Equations

• f.prod g = ∏ a ∈ f.support, g a (f a)

def Finsupp.sum {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] (f : α →₀ M) (g : α → M → N) : N

sum f g is the sum of g a (f a) over the support of f.

Equations

• f.sum g = ∑ a ∈ f.support, g a (f a)

theorem Finsupp.prod_of_support_subset {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] (f : α →₀ M) {s : Finset α} (hs : f.support ⊆ s) (g : α → M → N) (h : ∀ i ∈ s, g i 0 = 1) : f.prod g = ∏ x ∈ s, g x (f x)

theorem Finsupp.sum_of_support_subset {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] (f : α →₀ M) {s : Finset α} (hs : f.support ⊆ s) (g : α → M → N) (h : ∀ i ∈ s, g i 0 = 0) : f.sum g = ∑ x ∈ s, g x (f x)

theorem Finsupp.prod_fintype {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] [Fintype α] (f : α →₀ M) (g : α → M → N) (h : ∀ (i : α), g i 0 = 1) : f.prod g = ∏ i : α, g i (f i)

theorem Finsupp.sum_fintype {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] [Fintype α] (f : α →₀ M) (g : α → M → N) (h : ∀ (i : α), g i 0 = 0) : f.sum g = ∑ i : α, g i (f i)

@[simp]

theorem Finsupp.prod_single_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {a : α} {b : M} {h : α → M → N} (h_zero : h a 0 = 1) : (single a b).prod h = h a b

@[simp]

theorem Finsupp.sum_single_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {a : α} {b : M} {h : α → M → N} (h_zero : h a 0 = 0) : (single a b).sum h = h a b

theorem Finsupp.prod_mapRange_index {α : Type u_1} {M : Type u_8} {M' : Type u_9} {N : Type u_10} [Zero M] [Zero M'] [CommMonoid N] {f : M → M'} {hf : f 0 = 0} {g : α →₀ M} {h : α → M' → N} (h0 : ∀ (a : α), h a 0 = 1) : (mapRange f hf g).prod h = g.prod fun (a : α) (b : M) => h a (f b)

theorem Finsupp.sum_mapRange_index {α : Type u_1} {M : Type u_8} {M' : Type u_9} {N : Type u_10} [Zero M] [Zero M'] [AddCommMonoid N] {f : M → M'} {hf : f 0 = 0} {g : α →₀ M} {h : α → M' → N} (h0 : ∀ (a : α), h a 0 = 0) : (mapRange f hf g).sum h = g.sum fun (a : α) (b : M) => h a (f b)

@[simp]

theorem Finsupp.prod_zero_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {h : α → M → N} : prod 0 h = 1

@[simp]

theorem Finsupp.sum_zero_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {h : α → M → N} : sum 0 h = 0

theorem Finsupp.prod_comm {α : Type u_1} {β : Type u_7} {M : Type u_8} {M' : Type u_9} {N : Type u_10} [Zero M] [Zero M'] [CommMonoid N] (f : α →₀ M) (g : β →₀ M') (h : α → M → β → M' → N) : (f.prod fun (x : α) (v : M) => g.prod fun (x' : β) (v' : M') => h x v x' v') = g.prod fun (x' : β) (v' : M') => f.prod fun (x : α) (v : M) => h x v x' v'

theorem Finsupp.sum_comm {α : Type u_1} {β : Type u_7} {M : Type u_8} {M' : Type u_9} {N : Type u_10} [Zero M] [Zero M'] [AddCommMonoid N] (f : α →₀ M) (g : β →₀ M') (h : α → M → β → M' → N) : (f.sum fun (x : α) (v : M) => g.sum fun (x' : β) (v' : M') => h x v x' v') = g.sum fun (x' : β) (v' : M') => f.sum fun (x : α) (v : M) => h x v x' v'

@[simp]

theorem Finsupp.prod_ite_eq {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] [DecidableEq α] (f : α →₀ M) (a : α) (b : α → M → N) : (f.prod fun (x : α) (v : M) => if a = x then b x v else 1) = if a ∈ f.support then b a (f a) else 1

@[simp]

theorem Finsupp.sum_ite_eq {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] [DecidableEq α] (f : α →₀ M) (a : α) (b : α → M → N) : (f.sum fun (x : α) (v : M) => if a = x then b x v else 0) = if a ∈ f.support then b a (f a) else 0

theorem Finsupp.sum_ite_self_eq {α : Type u_1} [DecidableEq α] {N : Type u_16} [AddCommMonoid N] (f : α →₀ N) (a : α) : (f.sum fun (x : α) (v : N) => if a = x then v else 0) = f a

@[simp]

theorem Finsupp.if_mem_support {α : Type u_1} [DecidableEq α] {N : Type u_16} [Zero N] (f : α →₀ N) (a : α) : (if a ∈ f.support then f a else 0) = f a

The left-hand side of sum_ite_self_eq simplifies; this is the variant that is useful for simp.

@[simp]

theorem Finsupp.prod_ite_eq' {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] [DecidableEq α] (f : α →₀ M) (a : α) (b : α → M → N) : (f.prod fun (x : α) (v : M) => if x = a then b x v else 1) = if a ∈ f.support then b a (f a) else 1

A restatement of prod_ite_eq with the equality test reversed.

@[simp]

theorem Finsupp.sum_ite_eq' {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] [DecidableEq α] (f : α →₀ M) (a : α) (b : α → M → N) : (f.sum fun (x : α) (v : M) => if x = a then b x v else 0) = if a ∈ f.support then b a (f a) else 0

A restatement of sum_ite_eq with the equality test reversed.

theorem Finsupp.sum_ite_self_eq' {α : Type u_1} [DecidableEq α] {N : Type u_16} [AddCommMonoid N] (f : α →₀ N) (a : α) : (f.sum fun (x : α) (v : N) => if x = a then v else 0) = f a

A restatement of sum_ite_self_eq with the equality test reversed.

@[simp]

theorem Finsupp.prod_pow {α : Type u_1} {N : Type u_10} [CommMonoid N] [Fintype α] (f : α →₀ ℕ) (g : α → N) : (f.prod fun (a : α) (b : ℕ) => g a ^ b) = ∏ a : α, g a ^ f a

@[simp]

theorem Finsupp.sum_nsmul {α : Type u_1} {N : Type u_10} [AddCommMonoid N] [Fintype α] (f : α →₀ ℕ) (g : α → N) : (f.sum fun (a : α) (b : ℕ) => b • g a) = ∑ a : α, f a • g a

@[simp]

theorem Finsupp.prod_zpow {α : Type u_1} {N : Type u_16} [DivisionCommMonoid N] [Fintype α] (f : α →₀ ℤ) (g : α → N) : (f.prod fun (a : α) (b : ℤ) => g a ^ b) = ∏ a : α, g a ^ f a

@[simp]

theorem Finsupp.sum_zsmul {α : Type u_1} {N : Type u_16} [SubtractionCommMonoid N] [Fintype α] (f : α →₀ ℤ) (g : α → N) : (f.sum fun (a : α) (b : ℤ) => b • g a) = ∑ a : α, f a • g a

theorem Finsupp.onFinset_prod {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {s : Finset α} {f : α → M} {g : α → M → N} (hf : ∀ (a : α), f a ≠ 0 → a ∈ s) (hg : ∀ (a : α), g a 0 = 1) : (onFinset s f hf).prod g = ∏ a ∈ s, g a (f a)

If g maps a second argument of 0 to 1, then multiplying it over the result of onFinset is the same as multiplying it over the original Finset.

theorem Finsupp.onFinset_sum {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {s : Finset α} {f : α → M} {g : α → M → N} (hf : ∀ (a : α), f a ≠ 0 → a ∈ s) (hg : ∀ (a : α), g a 0 = 0) : (onFinset s f hf).sum g = ∑ a ∈ s, g a (f a)

If g maps a second argument of 0 to 0, summing it over the result of onFinset is the same as summing it over the original Finset.

theorem Finsupp.mul_prod_erase {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] (f : α →₀ M) (y : α) (g : α → M → N) (hyf : y ∈ f.support) : g y (f y) * (erase y f).prod g = f.prod g

Taking a product over f : α →₀ M is the same as multiplying the value on a single element y ∈ f.support by the product over erase y f.

theorem Finsupp.add_sum_erase {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] (f : α →₀ M) (y : α) (g : α → M → N) (hyf : y ∈ f.support) : g y (f y) + (erase y f).sum g = f.sum g

Taking a sum over f : α →₀ M is the same as adding the value on a single element y ∈ f.support to the sum over erase y f.

theorem Finsupp.mul_prod_erase' {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] (f : α →₀ M) (y : α) (g : α → M → N) (hg : ∀ (i : α), g i 0 = 1) : g y (f y) * (erase y f).prod g = f.prod g

Generalization of Finsupp.mul_prod_erase: if g maps a second argument of 0 to 1, then its product over f : α →₀ M is the same as multiplying the value on any element y : α by the product over erase y f.

theorem Finsupp.add_sum_erase' {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] (f : α →₀ M) (y : α) (g : α → M → N) (hg : ∀ (i : α), g i 0 = 0) : g y (f y) + (erase y f).sum g = f.sum g

Generalization of Finsupp.add_sum_erase: if g maps a second argument of 0 to 0, then its sum over f : α →₀ M is the same as adding the value on any element y : α to the sum over erase y f.

theorem SubmonoidClass.finsuppProd_mem {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {S : Type u_16} [SetLike S N] [SubmonoidClass S N] (s : S) (f : α →₀ M) (g : α → M → N) (h : ∀ (c : α), f c ≠ 0 → g c (f c) ∈ s) : f.prod g ∈ s

theorem AddSubmonoidClass.finsuppSum_mem {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {S : Type u_16} [SetLike S N] [AddSubmonoidClass S N] (s : S) (f : α →₀ M) (g : α → M → N) (h : ∀ (c : α), f c ≠ 0 → g c (f c) ∈ s) : f.sum g ∈ s

@[deprecated SubmonoidClass.finsuppProd_mem (since := "2025-04-06")]

theorem SubmonoidClass.finsupp_prod_mem {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {S : Type u_16} [SetLike S N] [SubmonoidClass S N] (s : S) (f : α →₀ M) (g : α → M → N) (h : ∀ (c : α), f c ≠ 0 → g c (f c) ∈ s) : f.prod g ∈ s

Alias of SubmonoidClass.finsuppProd_mem.

theorem Finsupp.prod_congr {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {f : α →₀ M} {g1 g2 : α → M → N} (h : ∀ x ∈ f.support, g1 x (f x) = g2 x (f x)) : f.prod g1 = f.prod g2

theorem Finsupp.sum_congr {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {f : α →₀ M} {g1 g2 : α → M → N} (h : ∀ x ∈ f.support, g1 x (f x) = g2 x (f x)) : f.sum g1 = f.sum g2

theorem Finsupp.prod_eq_single {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {f : α →₀ M} (a : α) {g : α → M → N} (h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1) (h₁ : f a = 0 → g a 0 = 1) : f.prod g = g a (f a)

theorem Finsupp.sum_eq_single {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {f : α →₀ M} (a : α) {g : α → M → N} (h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 0) (h₁ : f a = 0 → g a 0 = 0) : f.sum g = g a (f a)

@[simp]

theorem Finsupp.prod_eq_zero_iff {α : Type u_1} {ι : Type u_2} {β : Type u_7} [Zero α] [CommMonoidWithZero β] [Nontrivial β] [NoZeroDivisors β] {f : ι →₀ α} {g : ι → α → β} : f.prod g = 0 ↔ ∃ i ∈ f.support, g i (f i) = 0

theorem Finsupp.prod_ne_zero_iff {α : Type u_1} {ι : Type u_2} {β : Type u_7} [Zero α] [CommMonoidWithZero β] [Nontrivial β] [NoZeroDivisors β] {f : ι →₀ α} {g : ι → α → β} : f.prod g ≠ 0 ↔ ∀ i ∈ f.support, g i (f i) ≠ 0

theorem map_finsuppProd {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [Zero M] [CommMonoid N] [CommMonoid P] {H : Type u_16} [FunLike H N P] [MonoidHomClass H N P] (h : H) (f : α →₀ M) (g : α → M → N) : h (f.prod g) = f.prod fun (a : α) (b : M) => h (g a b)

theorem map_finsuppSum {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [Zero M] [AddCommMonoid N] [AddCommMonoid P] {H : Type u_16} [FunLike H N P] [AddMonoidHomClass H N P] (h : H) (f : α →₀ M) (g : α → M → N) : h (f.sum g) = f.sum fun (a : α) (b : M) => h (g a b)

@[deprecated map_finsuppProd (since := "2025-04-06")]

theorem map_finsupp_prod {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [Zero M] [CommMonoid N] [CommMonoid P] {H : Type u_16} [FunLike H N P] [MonoidHomClass H N P] (h : H) (f : α →₀ M) (g : α → M → N) : h (f.prod g) = f.prod fun (a : α) (b : M) => h (g a b)

Alias of map_finsuppProd.

@[deprecated map_finsuppSum (since := "2025-04-06")]

theorem map_finsupp_sum {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [Zero M] [AddCommMonoid N] [AddCommMonoid P] {H : Type u_16} [FunLike H N P] [AddMonoidHomClass H N P] (h : H) (f : α →₀ M) (g : α → M → N) : h (f.sum g) = f.sum fun (a : α) (b : M) => h (g a b)

Alias of map_finsuppSum.

theorem MonoidHom.coe_finsuppProd {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [Zero β] [MulOneClass N] [CommMonoid P] (f : α →₀ β) (g : α → β → N →* P) : ⇑(f.prod g) = f.prod fun (i : α) (fi : β) => ⇑(g i fi)

theorem AddMonoidHom.coe_finsuppSum {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [Zero β] [AddZeroClass N] [AddCommMonoid P] (f : α →₀ β) (g : α → β → N →+ P) : ⇑(f.sum g) = f.sum fun (i : α) (fi : β) => ⇑(g i fi)

@[deprecated MonoidHom.coe_finsuppProd (since := "2025-04-06")]

theorem MonoidHom.coe_finsupp_prod {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [Zero β] [MulOneClass N] [CommMonoid P] (f : α →₀ β) (g : α → β → N →* P) : ⇑(f.prod g) = f.prod fun (i : α) (fi : β) => ⇑(g i fi)

Alias of MonoidHom.coe_finsuppProd.

@[deprecated AddMonoidHom.coe_finsuppSum (since := "2025-04-06")]

theorem AddMonoidHom.coe_finsupp_sum {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [Zero β] [AddZeroClass N] [AddCommMonoid P] (f : α →₀ β) (g : α → β → N →+ P) : ⇑(f.sum g) = f.sum fun (i : α) (fi : β) => ⇑(g i fi)

Alias of AddMonoidHom.coe_finsuppSum.

@[simp]

theorem MonoidHom.finsuppProd_apply {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [Zero β] [MulOneClass N] [CommMonoid P] (f : α →₀ β) (g : α → β → N →* P) (x : N) : (f.prod g) x = f.prod fun (i : α) (fi : β) => (g i fi) x

@[simp]

theorem AddMonoidHom.finsuppSum_apply {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [Zero β] [AddZeroClass N] [AddCommMonoid P] (f : α →₀ β) (g : α → β → N →+ P) (x : N) : (f.sum g) x = f.sum fun (i : α) (fi : β) => (g i fi) x

@[deprecated MonoidHom.finsuppProd_apply (since := "2025-04-06")]

theorem MonoidHom.finsupp_prod_apply {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [Zero β] [MulOneClass N] [CommMonoid P] (f : α →₀ β) (g : α → β → N →* P) (x : N) : (f.prod g) x = f.prod fun (i : α) (fi : β) => (g i fi) x

Alias of MonoidHom.finsuppProd_apply.

@[deprecated AddMonoidHom.finsuppSum_apply (since := "2025-04-06")]

theorem AddMonoidHom.finsupp_sum_apply {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [Zero β] [AddZeroClass N] [AddCommMonoid P] (f : α →₀ β) (g : α → β → N →+ P) (x : N) : (f.sum g) x = f.sum fun (i : α) (fi : β) => (g i fi) x

Alias of AddMonoidHom.finsuppSum_apply.

theorem Finsupp.single_multiset_sum {α : Type u_1} {M : Type u_8} [AddCommMonoid M] (s : Multiset M) (a : α) : single a s.sum = (Multiset.map (single a) s).sum

theorem Finsupp.single_finset_sum {α : Type u_1} {ι : Type u_2} {M : Type u_8} [AddCommMonoid M] (s : Finset ι) (f : ι → M) (a : α) : single a (∑ b ∈ s, f b) = ∑ b ∈ s, single a (f b)

theorem Finsupp.single_sum {α : Type u_1} {ι : Type u_2} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] (s : ι →₀ M) (f : ι → M → N) (a : α) : single a (s.sum f) = s.sum fun (d : ι) (c : M) => single a (f d c)

theorem Finsupp.prod_neg_index {α : Type u_1} {M : Type u_8} {G : Type u_12} [SubtractionMonoid G] [CommMonoid M] {g : α →₀ G} {h : α → G → M} (h0 : ∀ (a : α), h a 0 = 1) : (-g).prod h = g.prod fun (a : α) (b : G) => h a (-b)

theorem Finsupp.sum_neg_index {α : Type u_1} {M : Type u_8} {G : Type u_12} [SubtractionMonoid G] [AddCommMonoid M] {g : α →₀ G} {h : α → G → M} (h0 : ∀ (a : α), h a 0 = 0) : (-g).sum h = g.sum fun (a : α) (b : G) => h a (-b)

theorem Finsupp.finset_sum_apply {α : Type u_1} {ι : Type u_2} {N : Type u_10} [AddCommMonoid N] (S : Finset ι) (f : ι → α →₀ N) (a : α) : (∑ i ∈ S, f i) a = ∑ i ∈ S, (f i) a

@[simp]

theorem Finsupp.sum_apply {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {f : α →₀ M} {g : α → M → β →₀ N} {a₂ : β} : (f.sum g) a₂ = f.sum fun (a₁ : α) (b : M) => (g a₁ b) a₂

@[simp]

theorem Finsupp.coe_finset_sum {α : Type u_1} {ι : Type u_2} {N : Type u_10} [AddCommMonoid N] (S : Finset ι) (f : ι → α →₀ N) : ⇑(∑ i ∈ S, f i) = ∑ i ∈ S, ⇑(f i)

@[simp]

theorem Finsupp.coe_sum {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] (f : α →₀ M) (g : α → M → β →₀ N) : ⇑(f.sum g) = f.sum fun (a₁ : α) (b : M) => ⇑(g a₁ b)

theorem Finsupp.support_sum {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [DecidableEq β] [Zero M] [AddCommMonoid N] {f : α →₀ M} {g : α → M → β →₀ N} : (f.sum g).support ⊆ f.support.biUnion fun (a : α) => (g a (f a)).support

theorem Finsupp.support_finset_sum {α : Type u_1} {β : Type u_7} {M : Type u_8} [DecidableEq β] [AddCommMonoid M] {s : Finset α} {f : α → β →₀ M} : (s.sum f).support ⊆ s.biUnion fun (x : α) => (f x).support

@[simp]

theorem Finsupp.sum_zero {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {f : α →₀ M} : (f.sum fun (x : α) (x : M) => 0) = 0

@[simp]

theorem Finsupp.prod_mul {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {f : α →₀ M} {h₁ h₂ : α → M → N} : (f.prod fun (a : α) (b : M) => h₁ a b * h₂ a b) = f.prod h₁ * f.prod h₂

@[simp]

theorem Finsupp.sum_add {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {f : α →₀ M} {h₁ h₂ : α → M → N} : (f.sum fun (a : α) (b : M) => h₁ a b + h₂ a b) = f.sum h₁ + f.sum h₂

@[simp]

theorem Finsupp.prod_inv {α : Type u_1} {M : Type u_8} {G : Type u_12} [Zero M] [CommGroup G] {f : α →₀ M} {h : α → M → G} : (f.prod fun (a : α) (b : M) => (h a b)⁻¹) = (f.prod h)⁻¹

@[simp]

theorem Finsupp.sum_neg {α : Type u_1} {M : Type u_8} {G : Type u_12} [Zero M] [AddCommGroup G] {f : α →₀ M} {h : α → M → G} : (f.sum fun (a : α) (b : M) => -h a b) = -f.sum h

@[simp]

theorem Finsupp.sum_sub {α : Type u_1} {M : Type u_8} {G : Type u_12} [Zero M] [SubtractionCommMonoid G] {f : α →₀ M} {h₁ h₂ : α → M → G} : (f.sum fun (a : α) (b : M) => h₁ a b - h₂ a b) = f.sum h₁ - f.sum h₂

theorem Finsupp.prod_add_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [DecidableEq α] [AddZeroClass M] [CommMonoid N] {f g : α →₀ M} {h : α → M → N} (h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1) (h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂) : (f + g).prod h = f.prod h * g.prod h

Taking the product under h is an additive-to-multiplicative homomorphism of finsupps, if h is an additive-to-multiplicative homomorphism on the support. This is a more general version of Finsupp.prod_add_index'; the latter has simpler hypotheses.

theorem Finsupp.sum_add_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [DecidableEq α] [AddZeroClass M] [AddCommMonoid N] {f g : α →₀ M} {h : α → M → N} (h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0) (h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) : (f + g).sum h = f.sum h + g.sum h

Taking the product under h is an additive homomorphism of finsupps, if h is an additive homomorphism on the support. This is a more general version of Finsupp.sum_add_index'; the latter has simpler hypotheses.

theorem Finsupp.prod_add_index' {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [CommMonoid N] {f g : α →₀ M} {h : α → M → N} (h_zero : ∀ (a : α), h a 0 = 1) (h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂) : (f + g).prod h = f.prod h * g.prod h

Taking the product under h is an additive-to-multiplicative homomorphism of finsupps, if h is an additive-to-multiplicative homomorphism. This is a more specialized version of Finsupp.prod_add_index with simpler hypotheses.

theorem Finsupp.sum_add_index' {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [AddCommMonoid N] {f g : α →₀ M} {h : α → M → N} (h_zero : ∀ (a : α), h a 0 = 0) (h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) : (f + g).sum h = f.sum h + g.sum h

Taking the sum under h is an additive homomorphism of finsupps,if h is an additive homomorphism. This is a more specific version of Finsupp.sum_add_index with simpler hypotheses.

@[simp]

theorem Finsupp.sum_hom_add_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [AddCommMonoid N] {f g : α →₀ M} (h : α → M →+ N) : ((f + g).sum fun (x : α) => ⇑(h x)) = (f.sum fun (x : α) => ⇑(h x)) + g.sum fun (x : α) => ⇑(h x)

@[simp]

theorem Finsupp.prod_hom_add_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [CommMonoid N] {f g : α →₀ M} (h : α → Multiplicative M →* N) : ((f + g).prod fun (a : α) (b : M) => (h a) (Multiplicative.ofAdd b)) = (f.prod fun (a : α) (b : M) => (h a) (Multiplicative.ofAdd b)) * g.prod fun (a : α) (b : M) => (h a) (Multiplicative.ofAdd b)

def Finsupp.liftAddHom {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [AddCommMonoid N] : (α → M →+ N) ≃+ ((α →₀ M) →+ N)

The canonical isomorphism between families of additive monoid homomorphisms α → (M →+ N) and monoid homomorphisms (α →₀ M) →+ N.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finsupp.liftAddHom_apply {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [AddCommMonoid N] (F : α → M →+ N) (f : α →₀ M) : (liftAddHom F) f = f.sum fun (x : α) => ⇑(F x)

@[simp]

theorem Finsupp.liftAddHom_symm_apply {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [AddCommMonoid N] (F : (α →₀ M) →+ N) (x : α) : liftAddHom.symm F x = F.comp (singleAddHom x)

theorem Finsupp.liftAddHom_symm_apply_apply {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [AddCommMonoid N] (F : (α →₀ M) →+ N) (x : α) (y : M) : (liftAddHom.symm F x) y = F (single x y)

@[simp]

theorem Finsupp.liftAddHom_singleAddHom {α : Type u_1} {M : Type u_8} [AddCommMonoid M] : liftAddHom singleAddHom = AddMonoidHom.id (α →₀ M)

@[simp]

theorem Finsupp.sum_single {α : Type u_1} {M : Type u_8} [AddCommMonoid M] (f : α →₀ M) : f.sum single = f

@[simp]

theorem Finsupp.univ_sum_single {α : Type u_1} {M : Type u_8} [Fintype α] [AddCommMonoid M] (f : α →₀ M) : ∑ a : α, single a (f a) = f

The Finsupp version of Finset.univ_sum_single

@[simp]

theorem Finsupp.univ_sum_single_apply {α : Type u_1} {M : Type u_8} [AddCommMonoid M] [Fintype α] (i : α) (m : M) : ∑ j : α, (single i m) j = m

@[simp]

theorem Finsupp.univ_sum_single_apply' {α : Type u_1} {M : Type u_8} [AddCommMonoid M] [Fintype α] (i : α) (m : M) : ∑ j : α, (single j m) i = m

theorem Finsupp.equivFunOnFinite_symm_eq_sum {α : Type u_1} {M : Type u_8} [Fintype α] [AddCommMonoid M] (f : α → M) : equivFunOnFinite.symm f = ∑ a : α, single a (f a)

theorem Finsupp.liftAddHom_apply_single {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [AddCommMonoid N] (f : α → M →+ N) (a : α) (b : M) : (liftAddHom f) (single a b) = (f a) b

@[simp]

theorem Finsupp.liftAddHom_comp_single {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [AddCommMonoid N] (f : α → M →+ N) (a : α) : (liftAddHom f).comp (singleAddHom a) = f a

theorem Finsupp.comp_liftAddHom {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [AddZeroClass M] [AddCommMonoid N] [AddCommMonoid P] (g : N →+ P) (f : α → M →+ N) : g.comp (liftAddHom f) = liftAddHom fun (a : α) => g.comp (f a)

theorem Finsupp.sum_sub_index {α : Type u_1} {γ : Type u_3} {β : Type u_7} [AddGroup β] [AddCommGroup γ] {f g : α →₀ β} {h : α → β → γ} (h_sub : ∀ (a : α) (b₁ b₂ : β), h a (b₁ - b₂) = h a b₁ - h a b₂) : (f - g).sum h = f.sum h - g.sum h

theorem Finsupp.prod_embDomain {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {v : α →₀ M} {f : α ↪ β} {g : β → M → N} : (embDomain f v).prod g = v.prod fun (a : α) (b : M) => g (f a) b

theorem Finsupp.sum_embDomain {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {v : α →₀ M} {f : α ↪ β} {g : β → M → N} : (embDomain f v).sum g = v.sum fun (a : α) (b : M) => g (f a) b

theorem Finsupp.prod_finset_sum_index {α : Type u_1} {ι : Type u_2} {M : Type u_8} {N : Type u_10} [AddCommMonoid M] [CommMonoid N] {s : Finset ι} {g : ι → α →₀ M} {h : α → M → N} (h_zero : ∀ (a : α), h a 0 = 1) (h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂) : ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h

theorem Finsupp.sum_finset_sum_index {α : Type u_1} {ι : Type u_2} {M : Type u_8} {N : Type u_10} [AddCommMonoid M] [AddCommMonoid N] {s : Finset ι} {g : ι → α →₀ M} {h : α → M → N} (h_zero : ∀ (a : α), h a 0 = 0) (h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) : ∑ i ∈ s, (g i).sum h = (∑ i ∈ s, g i).sum h

theorem Finsupp.prod_sum_index {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} {P : Type u_11} [Zero M] [AddCommMonoid N] [CommMonoid P] {f : α →₀ M} {g : α → M → β →₀ N} {h : β → N → P} (h_zero : ∀ (a : β), h a 0 = 1) (h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ * h a b₂) : (f.sum g).prod h = f.prod fun (a : α) (b : M) => (g a b).prod h

theorem Finsupp.sum_sum_index {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} {P : Type u_11} [Zero M] [AddCommMonoid N] [AddCommMonoid P] {f : α →₀ M} {g : α → M → β →₀ N} {h : β → N → P} (h_zero : ∀ (a : β), h a 0 = 0) (h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂) : (f.sum g).sum h = f.sum fun (a : α) (b : M) => (g a b).sum h

theorem Finsupp.multiset_sum_sum_index {α : 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 : α →₀ M) => g.sum h) f).sum

theorem Finsupp.support_sum_eq_biUnion {α : Type u_16} {ι : Type u_17} {M : Type u_18} [DecidableEq α] [AddCommMonoid M] {g : ι → α →₀ M} (s : Finset ι) (h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support) : (∑ i ∈ s, g i).support = s.biUnion fun (i : ι) => (g i).support

theorem Finsupp.multiset_map_sum {α : Type u_1} {γ : Type u_3} {β : Type u_7} {M : Type u_8} [Zero M] {f : α →₀ M} {m : β → γ} {h : α → M → Multiset β} : Multiset.map m (f.sum h) = f.sum fun (a : α) (b : M) => Multiset.map m (h a b)

theorem Finsupp.multiset_sum_sum {α : 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 : M) => (h a b).sum

theorem Finsupp.prod_add_index_of_disjoint {α : Type u_1} {M : Type u_8} [AddCommMonoid M] {f1 f2 : α →₀ M} (hd : Disjoint f1.support f2.support) {β : Type u_16} [CommMonoid β] (g : α → M → β) : (f1 + f2).prod g = f1.prod g * f2.prod g

For disjoint f1 and f2, and function g, the product of the products of g over f1 and f2 equals the product of g over f1 + f2

theorem Finsupp.sum_add_index_of_disjoint {α : Type u_1} {M : Type u_8} [AddCommMonoid M] {f1 f2 : α →₀ M} (hd : Disjoint f1.support f2.support) {β : Type u_16} [AddCommMonoid β] (g : α → M → β) : (f1 + f2).sum g = f1.sum g + f2.sum g

For disjoint f1 and f2, and function g, the sum of the sums of g over f1 and f2 equals the sum of g over f1 + f2

theorem Finsupp.prod_dvd_prod_of_subset_of_dvd {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {f1 f2 : α →₀ M} {g1 g2 : α → M → N} (h1 : f1.support ⊆ f2.support) (h2 : ∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)) : f1.prod g1 ∣ f2.prod g2

theorem Finsupp.indicator_eq_sum_attach_single {α : Type u_1} {M : Type u_8} [AddCommMonoid M] {s : Finset α} (f : (a : α) → a ∈ s → M) : indicator s f = ∑ x ∈ s.attach, single (↑x) (f ↑x ⋯)

theorem Finsupp.indicator_eq_sum_single {α : Type u_1} {M : Type u_8} [AddCommMonoid M] (s : Finset α) (f : α → M) : (indicator s fun (x : α) (x_1 : x ∈ s) => f x) = ∑ x ∈ s, single x (f x)

@[simp]

theorem Finsupp.prod_indicator_index_eq_prod_attach {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {s : Finset α} (f : (a : α) → a ∈ s → M) {h : α → M → N} (h_zero : ∀ a ∈ s, h a 0 = 1) : (indicator s f).prod h = ∏ x ∈ s.attach, h (↑x) (f ↑x ⋯)

@[simp]

theorem Finsupp.sum_indicator_index_eq_sum_attach {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {s : Finset α} (f : (a : α) → a ∈ s → M) {h : α → M → N} (h_zero : ∀ a ∈ s, h a 0 = 0) : (indicator s f).sum h = ∑ x ∈ s.attach, h (↑x) (f ↑x ⋯)

@[simp]

theorem Finsupp.prod_attach_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [CommMonoid N] {s : Finset α} (f : α → M) {h : α → M → N} : ∏ x ∈ s.attach, h (↑x) (f ↑x) = ∏ x ∈ s, h x (f x)

@[simp]

theorem Finsupp.sum_attach_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddCommMonoid N] {s : Finset α} (f : α → M) {h : α → M → N} : ∑ x ∈ s.attach, h (↑x) (f ↑x) = ∑ x ∈ s, h x (f x)

theorem Finsupp.prod_indicator_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {s : Finset α} (f : α → M) {h : α → M → N} (h_zero : ∀ a ∈ s, h a 0 = 1) : (indicator s fun (x : α) (x_1 : x ∈ s) => f x).prod h = ∏ x ∈ s, h x (f x)

theorem Finsupp.sum_indicator_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {s : Finset α} (f : α → M) {h : α → M → N} (h_zero : ∀ a ∈ s, h a 0 = 0) : (indicator s fun (x : α) (x_1 : x ∈ s) => f x).sum h = ∑ x ∈ s, h x (f x)

theorem Finsupp.prod_mul_eq_prod_mul_of_exists {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {f : α →₀ M} {g : α → M → N} {n₁ n₂ : N} (a : α) (ha : a ∈ f.support) (h : g a (f a) * n₁ = g a (f a) * n₂) : f.prod g * n₁ = f.prod g * n₂

theorem Finsupp.sum_add_eq_sum_add_of_exists {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {f : α →₀ M} {g : α → M → N} {n₁ n₂ : N} (a : α) (ha : a ∈ f.support) (h : g a (f a) + n₁ = g a (f a) + n₂) : f.sum g + n₁ = f.sum g + n₂

theorem Finset.sum_apply' {α : Type u_1} {ι : Type u_2} {A : Type u_4} [AddCommMonoid A] {s : Finset α} {f : α → ι →₀ A} (i : ι) : (∑ k ∈ s, f k) i = ∑ k ∈ s, (f k) i

theorem Finsupp.sum_apply' {ι : Type u_2} {γ : Type u_3} {A : Type u_4} {B : Type u_5} [AddCommMonoid A] [AddCommMonoid B] (g : ι →₀ A) (k : ι → A → γ → B) (x : γ) : g.sum k x = g.sum fun (i : ι) (b : A) => k i b x

theorem Finsupp.sum_apply'' {ι : Type u_2} {γ : Type u_3} {B : Type u_5} [AddCommMonoid B] {A : Type u_16} {F : Type u_17} [AddZeroClass A] [AddCommMonoid F] [FunLike F γ B] (g : ι →₀ A) (k : ι → A → F) (x : γ) (hg0 : ∀ (i : ι), k i 0 = 0) (hgadd : ∀ (i : ι) (a₁ a₂ : A), k i (a₁ + a₂) = k i a₁ + k i a₂) (h0 : 0 x = 0) (hadd : ∀ (f g : F), (f + g) x = f x + g x) : (g.sum k) x = g.sum fun (i : ι) (a : A) => (k i a) x

Version of Finsupp.sum_apply' that applies in large generality to linear combinations of functions in any FunLike type on which addition is defined pointwise.

At the time of writing Mathlib does not have a typeclass to express the condition that addition on a FunLike type is pointwise; hence this is asserted via explicit hypotheses.

theorem Finsupp.sum_sum_index' {α : Type u_1} {ι : Type u_2} {A : Type u_4} {C : Type u_6} [AddCommMonoid A] [AddCommMonoid C] {t : ι → A → C} {s : Finset α} {f : α → ι →₀ A} (h0 : ∀ (i : ι), t i 0 = 0) (h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y) : (∑ x ∈ s, f x).sum t = ∑ x ∈ s, (f x).sum t

theorem Finsupp.sum_mul {α : Type u_1} {R : Type u_14} {S : Type u_15} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (b : S) (s : α →₀ R) {f : α → R → S} : s.sum f * b = s.sum fun (a : α) (c : R) => f a c * b

theorem Finsupp.mul_sum {α : Type u_1} {R : Type u_14} {S : Type u_15} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (b : S) (s : α →₀ R) {f : α → R → S} : b * s.sum f = s.sum fun (a : α) (c : R) => b * f a c

@[simp]

theorem Multiset.card_finsuppSum {α : Type u_1} {ι : Type u_2} {M : Type u_8} [Zero M] (f : ι →₀ M) (g : ι → M → Multiset α) : (f.sum g).card = f.sum fun (i : ι) (m : M) => (g i m).card

theorem Nat.prod_pow_pos_of_zero_notMem_support {f : ℕ →₀ ℕ} (nhf : 0 ∉ f.support) : 0 < f.prod fun (x1 x2 : ℕ) => x1 ^ x2

If 0 : ℕ is not in the support of f : ℕ →₀ ℕ then 0 < ∏ x ∈ f.support, x ^ (f x).

@[deprecated Nat.prod_pow_pos_of_zero_notMem_support (since := "2025-05-23")]

theorem Nat.prod_pow_pos_of_zero_not_mem_support {f : ℕ →₀ ℕ} (nhf : 0 ∉ f.support) : 0 < f.prod fun (x1 x2 : ℕ) => x1 ^ x2

Alias of Nat.prod_pow_pos_of_zero_notMem_support.

---

If 0 : ℕ is not in the support of f : ℕ →₀ ℕ then 0 < ∏ x ∈ f.support, x ^ (f x).