Big operators for finsupps

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

Declarations about sum and prod

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

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.

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.

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 : α), i ∈ s → g i 0 = 0) : Finsupp.sum f g = Finset.sum s fun x => g x (↑f x)

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 : α), i ∈ s → g i 0 = 1) : Finsupp.prod f g = Finset.prod s fun x => g x (↑f x)

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) : Finsupp.sum f g = Finset.sum Finset.univ fun i => g i (↑f i)

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) : Finsupp.prod f g = Finset.prod Finset.univ fun i => g i (↑f i)

@[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) : Finsupp.sum (Finsupp.single a b) h = h a b

@[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) : Finsupp.prod (Finsupp.single a b) h = h a 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) : Finsupp.sum (Finsupp.mapRange f hf g) h = Finsupp.sum g fun a b => h a (f 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) : Finsupp.prod (Finsupp.mapRange f hf g) h = Finsupp.prod g fun a b => h a (f b)

@[simp]

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

@[simp]

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

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) : (Finsupp.sum f fun x v => Finsupp.sum g fun x' v' => h x v x' v') = Finsupp.sum g fun x' v' => Finsupp.sum f fun x v => h x v x' v'

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) : (Finsupp.prod f fun x v => Finsupp.prod g fun x' v' => h x v x' v') = Finsupp.prod g fun x' v' => Finsupp.prod f fun x v => h x v x' v'

@[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) : (Finsupp.sum f fun x v => if a = x then b x v else 0) = if a ∈ f.support then b a (↑f a) else 0

@[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) : (Finsupp.prod f fun x v => if a = x then b x v else 1) = if a ∈ f.support then b a (↑f a) else 1

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

@[simp]

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

@[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) : (Finsupp.sum f fun x v => 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.

@[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) : (Finsupp.prod f fun x v => 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.

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

@[simp]

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

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) : Finsupp.sum (Finsupp.onFinset s f hf) g = Finset.sum s fun a => 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.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) : Finsupp.prod (Finsupp.onFinset s f hf) g = Finset.prod s fun a => 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.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) + Finsupp.sum (Finsupp.erase y f) g = Finsupp.sum f g

Taking a sum over 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) (hyf : y ∈ f.support) : g y (↑f y) * Finsupp.prod (Finsupp.erase y f) g = Finsupp.prod f 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) (hg : ∀ (i : α), g i 0 = 0) : g y (↑f y) + Finsupp.sum (Finsupp.erase y f) g = Finsupp.sum f 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 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) * Finsupp.prod (Finsupp.erase y f) g = Finsupp.prod f 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 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) : Finsupp.sum f g ∈ s

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) : Finsupp.prod f g ∈ s

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

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

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} [AddMonoidHomClass H N P] (h : H) (f : α →₀ M) (g : α → M → N) : ↑h (Finsupp.sum f g) = Finsupp.sum f fun a b => ↑h (g a b)

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} [MonoidHomClass H N P] (h : H) (f : α →₀ M) (g : α → M → N) : ↑h (Finsupp.prod f g) = Finsupp.prod f fun a b => ↑h (g a b)

@[deprecated]

theorem AddEquiv.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 : N ≃+ P) (f : α →₀ M) (g : α → M → N) : ↑h (Finsupp.sum f g) = Finsupp.sum f fun a b => ↑h (g a b)

Deprecated, use _root_.map_finsupp_sum instead.

@[deprecated]

theorem MulEquiv.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 : N ≃* P) (f : α →₀ M) (g : α → M → N) : ↑h (Finsupp.prod f g) = Finsupp.prod f fun a b => ↑h (g a b)

Deprecated, use _root_.map_finsupp_prod instead.

@[deprecated]

theorem AddMonoidHom.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 : N →+ P) (f : α →₀ M) (g : α → M → N) : ↑h (Finsupp.sum f g) = Finsupp.sum f fun a b => ↑h (g a b)

Deprecated, use _root_.map_finsupp_sum instead.

@[deprecated]

theorem MonoidHom.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 : N →* P) (f : α →₀ M) (g : α → M → N) : ↑h (Finsupp.prod f g) = Finsupp.prod f fun a b => ↑h (g a b)

Deprecated, use _root_.map_finsupp_prod instead.

@[deprecated map_finsupp_sum]

theorem RingHom.map_finsupp_sum {α : Type u_1} {M : Type u_8} {R : Type u_14} {S : Type u_15} [Zero M] [Semiring R] [Semiring S] (h : R →+* S) (f : α →₀ M) (g : α → M → R) : ↑h (Finsupp.sum f g) = Finsupp.sum f fun a b => ↑h (g a b)

Deprecated, use _root_.map_finsupp_sum instead.

@[deprecated map_finsupp_prod]

theorem RingHom.map_finsupp_prod {α : Type u_1} {M : Type u_8} {R : Type u_14} {S : Type u_15} [Zero M] [CommSemiring R] [CommSemiring S] (h : R →+* S) (f : α →₀ M) (g : α → M → R) : ↑h (Finsupp.prod f g) = Finsupp.prod f fun a b => ↑h (g a b)

Deprecated, use _root_.map_finsupp_prod instead.

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

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

@[simp]

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

@[simp]

theorem MonoidHom.finsupp_prod_apply {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [Zero β] [Monoid N] [CommMonoid P] (f : α →₀ β) (g : α → β → N →* P) (x : N) : ↑(Finsupp.prod f g) x = Finsupp.prod f 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 : α) : Finsupp.single a (Multiset.sum s) = Multiset.sum (Multiset.map (Finsupp.single a) s)

theorem Finsupp.single_finset_sum {α : Type u_1} {ι : Type u_2} {M : Type u_8} [AddCommMonoid M] (s : Finset ι) (f : ι → M) (a : α) : Finsupp.single a (Finset.sum s fun b => f b) = Finset.sum s fun b => Finsupp.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 : α) : Finsupp.single a (Finsupp.sum s f) = Finsupp.sum s fun d c => Finsupp.single a (f d c)

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

theorem Finsupp.prod_neg_index {α : Type u_1} {M : Type u_8} {G : Type u_12} [AddGroup G] [CommMonoid M] {g : α →₀ G} {h : α → G → M} (h0 : ∀ (a : α), h a 0 = 1) : Finsupp.prod (-g) h = Finsupp.prod g fun a b => 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 : α) : ↑(Finset.sum S fun i => f i) a = Finset.sum S fun i => ↑(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₂ : β} : ↑(Finsupp.sum f g) a₂ = Finsupp.sum f fun a₁ b => ↑(g a₁ b) a₂

theorem Finsupp.coe_finset_sum {α : Type u_1} {ι : Type u_2} {N : Type u_10} [AddCommMonoid N] (S : Finset ι) (f : ι → α →₀ N) : ↑(Finset.sum S fun i => f i) = Finset.sum S fun i => ↑(f i)

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) : ↑(Finsupp.sum f g) = Finsupp.sum f fun a₁ b => ↑(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} : (Finsupp.sum f g).support ⊆ Finset.biUnion f.support 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} : (Finset.sum s f).support ⊆ Finset.biUnion s 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} : (Finsupp.sum f fun x x => 0) = 0

@[simp]

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

@[simp]

theorem Finsupp.prod_mul {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {f : α →₀ M} {h₁ : α → M → N} {h₂ : α → M → N} : (Finsupp.prod f fun a b => h₁ a b * h₂ a b) = Finsupp.prod f h₁ * Finsupp.prod f 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} : (Finsupp.sum f fun a b => -h a b) = -Finsupp.sum f 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} : (Finsupp.prod f fun a b => (h a b)⁻¹) = (Finsupp.prod f h)⁻¹

@[simp]

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

theorem Finsupp.sum_add_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [DecidableEq α] [AddZeroClass M] [AddCommMonoid N] {f : α →₀ M} {g : α →₀ M} {h : α → M → N} (h_zero : ∀ (a : α), a ∈ f.support ∪ g.support → h a 0 = 0) (h_add : ∀ (a : α), a ∈ f.support ∪ g.support → ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) : Finsupp.sum (f + g) h = Finsupp.sum f h + Finsupp.sum g 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} [DecidableEq α] [AddZeroClass M] [CommMonoid N] {f : α →₀ M} {g : α →₀ M} {h : α → M → N} (h_zero : ∀ (a : α), a ∈ f.support ∪ g.support → h a 0 = 1) (h_add : ∀ (a : α), a ∈ f.support ∪ g.support → ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂) : Finsupp.prod (f + g) h = Finsupp.prod f h * Finsupp.prod g 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} [AddZeroClass M] [AddCommMonoid N] {f : α →₀ M} {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₂) : Finsupp.sum (f + g) h = Finsupp.sum f h + Finsupp.sum g 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.

theorem Finsupp.prod_add_index' {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [CommMonoid N] {f : α →₀ M} {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₂) : Finsupp.prod (f + g) h = Finsupp.prod f h * Finsupp.prod g 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.

@[simp]

theorem Finsupp.sum_hom_add_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [AddCommMonoid N] {f : α →₀ M} {g : α →₀ M} (h : α → M →+ N) : (Finsupp.sum (f + g) fun x => ↑(h x)) = (Finsupp.sum f fun x => ↑(h x)) + Finsupp.sum g 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 : α →₀ M} {g : α →₀ M} (h : α → Multiplicative M →* N) : (Finsupp.prod (f + g) fun a b => ↑(h a) (↑Multiplicative.ofAdd b)) = (Finsupp.prod f fun a b => ↑(h a) (↑Multiplicative.ofAdd b)) * Finsupp.prod g fun a b => ↑(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.

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem Finsupp.sum_univ_single {α : Type u_1} {M : Type u_8} [AddCommMonoid M] [Fintype α] (i : α) (m : M) : (Finset.sum Finset.univ fun j => ↑(Finsupp.single i m) j) = m

@[simp]

theorem Finsupp.sum_univ_single' {α : Type u_1} {M : Type u_8} [AddCommMonoid M] [Fintype α] (i : α) (m : M) : (Finset.sum Finset.univ fun j => ↑(Finsupp.single j m) i) = m

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

@[simp]

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

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

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

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} : Finsupp.sum (Finsupp.embDomain f v) g = Finsupp.sum v fun a b => g (↑f a) b

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} : Finsupp.prod (Finsupp.embDomain f v) g = Finsupp.prod v fun a b => g (↑f a) b

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₂) : (Finset.sum s fun i => Finsupp.sum (g i) h) = Finsupp.sum (Finset.sum s fun i => g i) h

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₂) : (Finset.prod s fun i => Finsupp.prod (g i) h) = Finsupp.prod (Finset.sum s fun i => g i) h

theorem Finsupp.sum_sum_index {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} {P : Type u_11} [AddCommMonoid 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₂) : Finsupp.sum (Finsupp.sum f g) h = Finsupp.sum f fun a b => Finsupp.sum (g a b) h

theorem Finsupp.prod_sum_index {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} {P : Type u_11} [AddCommMonoid 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₂) : Finsupp.prod (Finsupp.sum f g) h = Finsupp.prod f fun a b => Finsupp.prod (g a b) 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₂) : Finsupp.sum (Multiset.sum f) h = Multiset.sum (Multiset.map (fun g => Finsupp.sum g h) f)

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) : (Finset.sum s fun i => g i).support = Finset.biUnion s 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 (Finsupp.sum f h) = Finsupp.sum f fun a b => 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} : Multiset.sum (Finsupp.sum f h) = Finsupp.sum f fun a b => Multiset.sum (h a b)

theorem Finsupp.sum_add_index_of_disjoint {α : Type u_1} {M : Type u_8} [AddCommMonoid M] {f1 : α →₀ M} {f2 : α →₀ M} (hd : Disjoint f1.support f2.support) {β : Type u_16} [AddCommMonoid β] (g : α → M → β) : Finsupp.sum (f1 + f2) g = Finsupp.sum f1 g + Finsupp.sum f2 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_add_index_of_disjoint {α : Type u_1} {M : Type u_8} [AddCommMonoid M] {f1 : α →₀ M} {f2 : α →₀ M} (hd : Disjoint f1.support f2.support) {β : Type u_16} [CommMonoid β] (g : α → M → β) : Finsupp.prod (f1 + f2) g = Finsupp.prod f1 g * Finsupp.prod f2 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.prod_dvd_prod_of_subset_of_dvd {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddCommMonoid M] [CommMonoid N] {f1 : α →₀ M} {f2 : α →₀ M} {g1 : α → M → N} {g2 : α → M → N} (h1 : f1.support ⊆ f2.support) (h2 : ∀ (a : α), a ∈ f1.support → g1 a (↑f1 a) ∣ g2 a (↑f2 a)) : Finsupp.prod f1 g1 ∣ Finsupp.prod f2 g2

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

theorem Finsupp.indicator_eq_sum_single {α : Type u_1} {M : Type u_8} [AddCommMonoid M] (s : Finset α) (f : α → M) : (Finsupp.indicator s fun x x_1 => f x) = Finset.sum s fun x => Finsupp.single 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 : α), a ∈ s → h a 0 = 0) : Finsupp.sum (Finsupp.indicator s f) h = Finset.sum (Finset.attach s) fun x => h (↑x) (f ↑x (_ : ↑x ∈ s))

@[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 : α), a ∈ s → h a 0 = 1) : Finsupp.prod (Finsupp.indicator s f) h = Finset.prod (Finset.attach s) fun x => h (↑x) (f ↑x (_ : ↑x ∈ s))

@[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 : α), a ∈ s → h a 0 = 0) : Finsupp.sum (Finsupp.indicator s fun x x_1 => f x) h = Finset.sum s fun x => 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 : α), a ∈ s → h a 0 = 1) : Finsupp.prod (Finsupp.indicator s fun x x_1 => f x) h = Finset.prod s fun x => h x (f x)

theorem Finsupp.sum_cons {M : Type u_8} [AddCommMonoid M] (n : ℕ) (σ : Fin n →₀ M) (i : M) : (Finsupp.sum (Finsupp.cons i σ) fun x e => e) = i + Finsupp.sum σ fun x e => e

theorem Finsupp.sum_cons' {M : Type u_8} {N : Type u_10} [AddCommMonoid M] [AddCommMonoid N] (n : ℕ) (σ : Fin n →₀ M) (i : M) (f : Fin (n + 1) → M → N) (h : ∀ (x : Fin (n + 1)), f x 0 = 0) : Finsupp.sum (Finsupp.cons i σ) f = f 0 i + Finsupp.sum σ (Fin.tail f)

theorem Finset.sum_apply' {α : Type u_1} {ι : Type u_2} {A : Type u_4} [AddCommMonoid A] {s : Finset α} {f : α → ι →₀ A} (i : ι) : ↑(Finset.sum s fun k => f k) i = Finset.sum s fun k => ↑(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 : γ) : Finsupp.sum ι A (γ → B) AddMonoid.toZero Pi.addCommMonoid g k x = Finsupp.sum g fun i b => k i b x

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} (h0 : ∀ (i : ι), t i 0 = 0) (h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y) {s : Finset α} {f : α → ι →₀ A} : Finsupp.sum (Finset.sum s fun x => f x) t = Finset.sum s fun x => Finsupp.sum (f x) 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} : Finsupp.sum s f * b = Finsupp.sum s fun a c => 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 * Finsupp.sum s f = Finsupp.sum s fun a c => b * f a c

theorem Nat.prod_pow_pos_of_zero_not_mem_support {f : ℕ →₀ ℕ} (hf : ¬0 ∈ f.support) : 0 < Finsupp.prod f fun x x_1 => x ^ x_1

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