# mathlib3documentation

algebra.big_operators.finsupp

# Big operators for finsupps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

def finsupp.prod {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] [comm_monoid N] (f : α →₀ M) (g : α M N) :
N

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

Equations
def finsupp.sum {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] (f : α →₀ M) (g : α M N) :
N

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

Equations
theorem finsupp.prod_of_support_subset {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] [comm_monoid N] (f : α →₀ M) {s : finset α} (hs : f.support s) (g : α M N) (h : (i : α), i s g i 0 = 1) :
f.prod g = s.prod (λ (x : α), g x (f x))
theorem finsupp.sum_of_support_subset {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] (f : α →₀ M) {s : finset α} (hs : f.support s) (g : α M N) (h : (i : α), i s g i 0 = 0) :
f.sum g = s.sum (λ (x : α), g x (f x))
theorem finsupp.prod_fintype {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] [comm_monoid N] [fintype α] (f : α →₀ M) (g : α M N) (h : (i : α), g i 0 = 1) :
f.prod g = finset.univ.prod (λ (i : α), g i (f i))
theorem finsupp.sum_fintype {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] [fintype α] (f : α →₀ M) (g : α M N) (h : (i : α), g i 0 = 0) :
f.sum g = finset.univ.sum (λ (i : α), g i (f i))
@[simp]
theorem finsupp.prod_single_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] [comm_monoid N] {a : α} {b : M} {h : α M N} (h_zero : h a 0 = 1) :
b).prod h = h a b
@[simp]
theorem finsupp.sum_single_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] {a : α} {b : M} {h : α M N} (h_zero : h a 0 = 0) :
b).sum h = h a b
theorem finsupp.sum_map_range_index {α : Type u_1} {M : Type u_8} {M' : Type u_9} {N : Type u_10} [has_zero M] [has_zero M'] {f : M M'} {hf : f 0 = 0} {g : α →₀ M} {h : α M' N} (h0 : (a : α), h a 0 = 0) :
hf g).sum h = g.sum (λ (a : α) (b : M), h a (f b))
theorem finsupp.prod_map_range_index {α : Type u_1} {M : Type u_8} {M' : Type u_9} {N : Type u_10} [has_zero M] [has_zero M'] [comm_monoid N] {f : M M'} {hf : f 0 = 0} {g : α →₀ M} {h : α M' N} (h0 : (a : α), h a 0 = 1) :
hf g).prod h = g.prod (λ (a : α) (b : M), h a (f b))
@[simp]
theorem finsupp.prod_zero_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] [comm_monoid N] {h : α M N} :
0.prod h = 1
@[simp]
theorem finsupp.sum_zero_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] {h : α M N} :
0.sum h = 0
theorem finsupp.prod_comm {α : Type u_1} {β : Type u_7} {M : Type u_8} {M' : Type u_9} {N : Type u_10} [has_zero M] [has_zero M'] [comm_monoid N] (f : α →₀ M) (g : β →₀ M') (h : α M β M' N) :
f.prod (λ (x : α) (v : M), g.prod (λ (x' : β) (v' : M'), h x v x' v')) = g.prod (λ (x' : β) (v' : M'), f.prod (λ (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} [has_zero M] [has_zero M'] (f : α →₀ M) (g : β →₀ M') (h : α M β M' N) :
f.sum (λ (x : α) (v : M), g.sum (λ (x' : β) (v' : M'), h x v x' v')) = g.sum (λ (x' : β) (v' : M'), f.sum (λ (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} [has_zero M] [comm_monoid N] [decidable_eq α] (f : α →₀ M) (a : α) (b : α M N) :
f.prod (λ (x : α) (v : M), ite (a = x) (b x v) 1) = ite (a f.support) (b a (f a)) 1
@[simp]
theorem finsupp.sum_ite_eq {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] [decidable_eq α] (f : α →₀ M) (a : α) (b : α M N) :
f.sum (λ (x : α) (v : M), ite (a = x) (b x v) 0) = ite (a f.support) (b a (f a)) 0
@[simp]
theorem finsupp.sum_ite_self_eq {α : Type u_1} [decidable_eq α] {N : Type u_2} (f : α →₀ N) (a : α) :
f.sum (λ (x : α) (v : N), ite (a = x) v 0) = f a
@[simp]
theorem finsupp.prod_ite_eq' {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] [comm_monoid N] [decidable_eq α] (f : α →₀ M) (a : α) (b : α M N) :
f.prod (λ (x : α) (v : M), ite (x = a) (b x v) 1) = ite (a f.support) (b a (f a)) 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} [has_zero M] [decidable_eq α] (f : α →₀ M) (a : α) (b : α M N) :
f.sum (λ (x : α) (v : M), ite (x = a) (b x v) 0) = ite (a f.support) (b a (f a)) 0

A restatement of `sum_ite_eq` with the equality test reversed.

@[simp]
theorem finsupp.sum_ite_self_eq' {α : Type u_1} [decidable_eq α] {N : Type u_2} (f : α →₀ N) (a : α) :
f.sum (λ (x : α) (v : N), ite (x = a) v 0) = f a
@[simp]
theorem finsupp.prod_pow {α : Type u_1} {N : Type u_10} [comm_monoid N] [fintype α] (f : α →₀ ) (g : α N) :
f.prod (λ (a : α) (b : ), g a ^ b) = finset.univ.prod (λ (a : α), g a ^ f a)
theorem finsupp.on_finset_prod {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] [comm_monoid N] {s : finset α} {f : α M} {g : α M N} (hf : (a : α), f a 0 a s) (hg : (a : α), g a 0 = 1) :
hf).prod g = s.prod (λ (a : α), g a (f a))

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

theorem finsupp.on_finset_sum {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] {s : finset α} {f : α M} {g : α M N} (hf : (a : α), f a 0 a s) (hg : (a : α), g a 0 = 0) :
hf).sum g = s.sum (λ (a : α), g a (f a))

If `g` maps a second argument of 0 to 0, summing it over the result of `on_finset` 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} [has_zero M] [comm_monoid N] (f : α →₀ M) (y : α) (g : α M N) (hyf : y f.support) :
g y (f 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} [has_zero M] (f : α →₀ M) (y : α) (g : α M N) (hyf : y f.support) :
g y (f y) + f).sum g = f.sum 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} [has_zero M] [comm_monoid N] (f : α →₀ M) (y : α) (g : α M N) (hg : (i : α), g i 0 = 1) :
g y (f 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} [has_zero M] (f : α →₀ M) (y : α) (g : α M N) (hg : (i : α), g i 0 = 0) :
g y (f 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 add_submonoid_class.finsupp_sum_mem {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] {S : Type u_2} [ N] [ N] (s : S) (f : α →₀ M) (g : α M N) (h : (c : α), f c 0 g c (f c) s) :
f.sum g s
theorem submonoid_class.finsupp_prod_mem {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] [comm_monoid N] {S : Type u_2} [ N] [ N] (s : S) (f : α →₀ M) (g : α M N) (h : (c : α), f c 0 g c (f c) s) :
f.prod g s
theorem finsupp.prod_congr {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] [comm_monoid N] {f : α →₀ M} {g1 g2 : α M N} (h : (x : α), 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} [has_zero M] {f : α →₀ M} {g1 g2 : α M N} (h : (x : α), x f.support g1 x (f x) = g2 x (f x)) :
f.sum g1 = f.sum g2
theorem map_finsupp_sum {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [has_zero M] {H : Type u_2} [ P] (h : H) (f : α →₀ M) (g : α M N) :
h (f.sum g) = f.sum (λ (a : α) (b : M), h (g a b))
theorem map_finsupp_prod {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [has_zero M] [comm_monoid N] [comm_monoid P] {H : Type u_2} [ P] (h : H) (f : α →₀ M) (g : α M N) :
h (f.prod g) = f.prod (λ (a : α) (b : M), h (g a b))
@[protected]
theorem mul_equiv.map_finsupp_prod {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [has_zero M] [comm_monoid N] [comm_monoid P] (h : N ≃* P) (f : α →₀ M) (g : α M N) :
h (f.prod g) = f.prod (λ (a : α) (b : M), h (g a b))

Deprecated, use `_root_.map_finsupp_prod` instead.

@[protected]
theorem add_equiv.map_finsupp_sum {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [has_zero M] (h : N ≃+ P) (f : α →₀ M) (g : α M N) :
h (f.sum g) = f.sum (λ (a : α) (b : M), h (g a b))

Deprecated, use `_root_.map_finsupp_sum` instead.

@[protected]
theorem add_monoid_hom.map_finsupp_sum {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [has_zero M] (h : N →+ P) (f : α →₀ M) (g : α M N) :
h (f.sum g) = f.sum (λ (a : α) (b : M), h (g a b))

Deprecated, use `_root_.map_finsupp_sum` instead.

@[protected]
theorem monoid_hom.map_finsupp_prod {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [has_zero M] [comm_monoid N] [comm_monoid P] (h : N →* P) (f : α →₀ M) (g : α M N) :
h (f.prod g) = f.prod (λ (a : α) (b : M), h (g a b))

Deprecated, use `_root_.map_finsupp_prod` instead.

@[protected]
theorem ring_hom.map_finsupp_sum {α : Type u_1} {M : Type u_8} {R : Type u_14} {S : Type u_15} [has_zero M] [semiring R] [semiring S] (h : R →+* S) (f : α →₀ M) (g : α M R) :
h (f.sum g) = f.sum (λ (a : α) (b : M), h (g a b))

Deprecated, use `_root_.map_finsupp_sum` instead.

@[protected]
theorem ring_hom.map_finsupp_prod {α : Type u_1} {M : Type u_8} {R : Type u_14} {S : Type u_15} [has_zero M] (h : R →+* S) (f : α →₀ M) (g : α M R) :
h (f.prod g) = f.prod (λ (a : α) (b : M), h (g a b))

Deprecated, use `_root_.map_finsupp_prod` instead.

theorem add_monoid_hom.coe_finsupp_sum {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [has_zero β] [add_monoid N] (f : α →₀ β) (g : α β N →+ P) :
(f.sum g) = f.sum (λ (i : α) (fi : β), (g i fi))
theorem monoid_hom.coe_finsupp_prod {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [has_zero β] [monoid N] [comm_monoid P] (f : α →₀ β) (g : α β N →* P) :
(f.prod g) = f.prod (λ (i : α) (fi : β), (g i fi))
@[simp]
theorem monoid_hom.finsupp_prod_apply {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [has_zero β] [monoid N] [comm_monoid P] (f : α →₀ β) (g : α β N →* P) (x : N) :
(f.prod g) x = f.prod (λ (i : α) (fi : β), (g i fi) x)
@[simp]
theorem add_monoid_hom.finsupp_sum_apply {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [has_zero β] [add_monoid N] (f : α →₀ β) (g : α β N →+ P) (x : N) :
(f.sum g) x = f.sum (λ (i : α) (fi : β), (g i fi) x)
theorem finsupp.single_multiset_sum {α : Type u_1} {M : Type u_8} (s : multiset M) (a : α) :
= s).sum
theorem finsupp.single_finset_sum {α : Type u_1} {ι : Type u_2} {M : Type u_8} (s : finset ι) (f : ι M) (a : α) :
(s.sum (λ (b : ι), f b)) = s.sum (λ (b : ι), (f b))
theorem finsupp.single_sum {α : Type u_1} {ι : Type u_2} {M : Type u_8} {N : Type u_10} [has_zero M] (s : ι →₀ M) (f : ι M N) (a : α) :
(s.sum f) = s.sum (λ (d : ι) (c : M), (f d c))
theorem finsupp.prod_neg_index {α : Type u_1} {M : Type u_8} {G : Type u_12} [add_group G] [comm_monoid M] {g : α →₀ G} {h : α G M} (h0 : (a : α), h a 0 = 1) :
(-g).prod h = g.prod (λ (a : α) (b : G), h a (-b))
theorem finsupp.sum_neg_index {α : Type u_1} {M : Type u_8} {G : Type u_12} [add_group G] {g : α →₀ G} {h : α G M} (h0 : (a : α), h a 0 = 0) :
(-g).sum h = g.sum (λ (a : α) (b : G), h a (-b))
theorem finsupp.finset_sum_apply {α : Type u_1} {ι : Type u_2} {N : Type u_10} (S : finset ι) (f : ι α →₀ N) (a : α) :
(S.sum (λ (i : ι), f i)) a = S.sum (λ (i : ι), (f i) a)
@[simp]
theorem finsupp.sum_apply {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [has_zero M] {f : α →₀ M} {g : α M β →₀ N} {a₂ : β} :
(f.sum g) a₂ = f.sum (λ (a₁ : α) (b : M), (g a₁ b) a₂)
theorem finsupp.coe_finset_sum {α : Type u_1} {ι : Type u_2} {N : Type u_10} (S : finset ι) (f : ι α →₀ N) :
(S.sum (λ (i : ι), f i)) = S.sum (λ (i : ι), (f i))
theorem finsupp.coe_sum {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [has_zero M] (f : α →₀ M) (g : α M β →₀ N) :
(f.sum g) = f.sum (λ (a₁ : α) (b : M), (g a₁ b))
theorem finsupp.support_sum {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [decidable_eq β] [has_zero M] {f : α →₀ M} {g : α M β →₀ N} :
(f.sum g).support f.support.bUnion (λ (a : α), (g a (f a)).support)
theorem finsupp.support_finset_sum {α : Type u_1} {β : Type u_7} {M : Type u_8} [decidable_eq β] {s : finset α} {f : α β →₀ M} :
(s.sum f).support s.bUnion (λ (x : α), (f x).support)
@[simp]
theorem finsupp.sum_zero {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] {f : α →₀ M} :
f.sum (λ (a : α) (b : M), 0) = 0
@[simp]
theorem finsupp.sum_add {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] {f : α →₀ M} {h₁ h₂ : α M N} :
f.sum (λ (a : α) (b : M), h₁ a b + h₂ a b) = f.sum h₁ + f.sum h₂
@[simp]
theorem finsupp.prod_mul {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] [comm_monoid N] {f : α →₀ M} {h₁ h₂ : α M N} :
f.prod (λ (a : α) (b : M), h₁ a b * h₂ a b) = f.prod h₁ * f.prod h₂
@[simp]
theorem finsupp.prod_inv {α : Type u_1} {M : Type u_8} {G : Type u_12} [has_zero M] [comm_group G] {f : α →₀ M} {h : α M G} :
f.prod (λ (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} [has_zero M] {f : α →₀ M} {h : α M G} :
f.sum (λ (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} [has_zero M] {f : α →₀ M} {h₁ h₂ : α M G} :
f.sum (λ (a : α) (b : M), h₁ a b - h₂ a b) = f.sum h₁ - f.sum h₂
theorem finsupp.sum_add_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [decidable_eq α] {f 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₂) :
(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} [decidable_eq α] [comm_monoid N] {f 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₂) :
(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} {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.

theorem finsupp.prod_add_index' {α : Type u_1} {M : Type u_8} {N : Type u_10} [comm_monoid 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.

@[simp]
theorem finsupp.sum_hom_add_index {α : Type u_1} {M : Type u_8} {N : Type u_10} {f g : α →₀ M} (h : α M →+ N) :
(f + g).sum (λ (x : α), (h x)) = f.sum (λ (x : α), (h x)) + g.sum (λ (x : α), (h x))
@[simp]
theorem finsupp.prod_hom_add_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [comm_monoid N] {f g : α →₀ M} (h : α ) :
(f + g).prod (λ (a : α) (b : M), (h a) = f.prod (λ (a : α) (b : M), (h a) * g.prod (λ (a : α) (b : M), (h a)
noncomputable def finsupp.lift_add_hom {α : Type u_1} {M : Type u_8} {N : Type u_10}  :
M →+ N) ≃+ ((α →₀ M) →+ N)

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

Equations
@[simp]
theorem finsupp.lift_add_hom_apply {α : Type u_1} {M : Type u_8} {N : Type u_10} (F : α M →+ N) (f : α →₀ M) :
= f.sum (λ (x : α), (F x))
@[simp]
theorem finsupp.lift_add_hom_symm_apply {α : Type u_1} {M : Type u_8} {N : Type u_10} (F : →₀ M) →+ N) (x : α) :
=
theorem finsupp.lift_add_hom_symm_apply_apply {α : Type u_1} {M : Type u_8} {N : Type u_10} (F : →₀ M) →+ N) (x : α) (y : M) :
x) y = F y)
@[simp]
@[simp]
theorem finsupp.sum_single {α : Type u_1} {M : Type u_8} (f : α →₀ M) :
@[simp]
theorem finsupp.sum_univ_single {α : Type u_1} {M : Type u_8} [fintype α] (i : α) (m : M) :
finset.univ.sum (λ (j : α), m) j) = m
@[simp]
theorem finsupp.sum_univ_single' {α : Type u_1} {M : Type u_8} [fintype α] (i : α) (m : M) :
finset.univ.sum (λ (j : α), m) i) = m
@[simp]
theorem finsupp.lift_add_hom_apply_single {α : Type u_1} {M : Type u_8} {N : Type u_10} (f : α M →+ N) (a : α) (b : M) :
b) = (f a) b
@[simp]
theorem finsupp.lift_add_hom_comp_single {α : Type u_1} {M : Type u_8} {N : Type u_10} (f : α M →+ N) (a : α) :
= f a
theorem finsupp.comp_lift_add_hom {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} (g : N →+ P) (f : α M →+ N) :
= finsupp.lift_add_hom (λ (a : α), g.comp (f a))
theorem finsupp.sum_sub_index {α : Type u_1} {γ : Type u_3} {β : Type u_7} {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.sum_emb_domain {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [has_zero M] {v : α →₀ M} {f : α β} {g : β M N} :
v).sum g = v.sum (λ (a : α) (b : M), g (f a) b)
theorem finsupp.prod_emb_domain {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [has_zero M] [comm_monoid N] {v : α →₀ M} {f : α β} {g : β M N} :
v).prod g = v.prod (λ (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} [comm_monoid 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₂) :
s.prod (λ (i : ι), (g i).prod h) = (s.sum (λ (i : ι), g i)).prod h
theorem finsupp.sum_finset_sum_index {α : Type u_1} {ι : Type u_2} {M : Type u_8} {N : Type u_10} {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₂) :
s.sum (λ (i : ι), (g i).sum h) = (s.sum (λ (i : ι), g i)).sum h
theorem finsupp.sum_sum_index {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} {P : Type u_11} {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 (λ (a : α) (b : M), (g a b).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} [comm_monoid 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 (λ (a : α) (b : M), (g a b).prod h)
theorem finsupp.multiset_sum_sum_index {α : Type u_1} {M : Type u_8} {N : Type u_10} (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 (λ (g : α →₀ M), g.sum h) f).sum
theorem finsupp.support_sum_eq_bUnion {α : Type u_1} {ι : Type u_2} {M : Type u_3} [decidable_eq α] {g : ι α →₀ M} (s : finset ι) (h : (i₁ i₂ : ι), i₁ i₂ disjoint (g i₁).support (g i₂).support) :
(s.sum (λ (i : ι), g i)).support = s.bUnion (λ (i : ι), (g i).support)
theorem finsupp.multiset_map_sum {α : Type u_1} {γ : Type u_3} {β : Type u_7} {M : Type u_8} [has_zero M] {f : α →₀ M} {m : β γ} {h : α M } :
(f.sum h) = f.sum (λ (a : α) (b : M), (h a b))
theorem finsupp.multiset_sum_sum {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] {f : α →₀ M} {h : α M } :
(f.sum h).sum = f.sum (λ (a : α) (b : M), (h a b).sum)
theorem finsupp.sum_add_index_of_disjoint {α : Type u_1} {M : Type u_8} {f1 f2 : α →₀ M} (hd : f2.support) {β : Type u_2} (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_add_index_of_disjoint {α : Type u_1} {M : Type u_8} {f1 f2 : α →₀ M} (hd : f2.support) {β : Type u_2} [comm_monoid β] (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.prod_dvd_prod_of_subset_of_dvd {α : Type u_1} {M : Type u_8} {N : Type u_10} [comm_monoid N] {f1 f2 : α →₀ M} {g1 g2 : α M N} (h1 : f1.support f2.support) (h2 : (a : α), a f1.support g1 a (f1 a) g2 a (f2 a)) :
f1.prod g1 f2.prod g2
theorem finsupp.indicator_eq_sum_single {α : Type u_1} {M : Type u_8} (s : finset α) (f : Π (a : α), a s M) :
= s.attach.sum (λ (x : {x // x s}), (f x _))
@[simp]
theorem finsupp.prod_indicator_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] [comm_monoid N] {s : finset α} (f : Π (a : α), a s M) {h : α M N} (h_zero : (a : α), a s h a 0 = 1) :
f).prod h = s.attach.prod (λ (x : {x // x s}), h x (f x _))
@[simp]
theorem finsupp.sum_indicator_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] {s : finset α} (f : Π (a : α), a s M) {h : α M N} (h_zero : (a : α), a s h a 0 = 0) :
f).sum h = s.attach.sum (λ (x : {x // x s}), h x (f x _))
theorem finset.sum_apply' {α : Type u_1} {ι : Type u_2} {A : Type u_4} {s : finset α} {f : α ι →₀ A} (i : ι) :
(s.sum (λ (k : α), f k)) i = s.sum (λ (k : α), (f k) i)
theorem finsupp.sum_apply' {ι : Type u_2} {γ : Type u_3} {A : Type u_4} {B : Type u_5} (g : ι →₀ A) (k : ι A γ B) (x : γ) :
g.sum k x = g.sum (λ (i : ι) (b : A), k i b x)
theorem finsupp.sum_sum_index' {α : Type u_1} {ι : Type u_2} {A : Type u_4} {C : Type u_6} {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} :
(s.sum (λ (x : α), f x)).sum t = s.sum (λ (x : α), (f x).sum t)
theorem finsupp.sum_mul {α : Type u_1} {R : Type u_14} {S : Type u_15} (b : S) (s : α →₀ R) {f : α R S} :
s.sum f * b = s.sum (λ (a : α) (c : R), f a c * b)
theorem finsupp.mul_sum {α : Type u_1} {R : Type u_14} {S : Type u_15} (b : S) (s : α →₀ R) {f : α R S} :
b * s.sum f = s.sum (λ (a : α) (c : R), b * f a c)

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