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.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

theorem AddSubmonoidClass.finsupp_sum_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

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_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)

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)

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)

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)

@[simp]

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

@[simp]

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

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_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)

@[simp]

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.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_not_mem_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).