mathlib documentation

algebra.big_operators.finsupp

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 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] [add_comm_monoid N] (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] [add_comm_monoid N] (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] [add_comm_monoid N] [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) :
(finsupp.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} [has_zero M] [add_comm_monoid N] {a : α} {b : M} {h : α M N} (h_zero : h a 0 = 0) :
(finsupp.single a 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'] [add_comm_monoid N] {f : M M'} {hf : f 0 = 0} {g : α →₀ M} {h : α M' N} (h0 : (a : α), h a 0 = 0) :
(finsupp.map_range f 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) :
(finsupp.map_range f 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] [add_comm_monoid N] {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'] [add_comm_monoid N] (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] [add_comm_monoid N] [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} [add_comm_monoid N] (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] [add_comm_monoid N] [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} [add_comm_monoid N] (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) :
(finsupp.on_finset s f 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] [add_comm_monoid N] {s : finset α} {f : α M} {g : α M N} (hf : (a : α), f a 0 a s) (hg : (a : α), g a 0 = 0) :
(finsupp.on_finset s f 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) * (finsupp.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} [has_zero M] [add_comm_monoid N] (f : α →₀ M) (y : α) (g : α M N) (hyf : y f.support) :
g y (f y) + (finsupp.erase 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) * (finsupp.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} [has_zero M] [add_comm_monoid N] (f : α →₀ M) (y : α) (g : α M N) (hg : (i : α), g i 0 = 0) :
g y (f y) + (finsupp.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 add_submonoid_class.finsupp_sum_mem {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] [add_comm_monoid N] {S : Type u_2} [set_like S N] [add_submonoid_class S 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} [set_like S N] [submonoid_class S 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] [add_comm_monoid N] {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] [add_comm_monoid N] [add_comm_monoid P] {H : Type u_2} [add_monoid_hom_class H N 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} [monoid_hom_class H N 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] [add_comm_monoid N] [add_comm_monoid P] (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] [add_comm_monoid N] [add_comm_monoid P] (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] [comm_semiring R] [comm_semiring S] (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] [add_comm_monoid P] (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] [add_comm_monoid P] (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} [add_comm_monoid M] (s : multiset M) (a : α) :
theorem finsupp.single_finset_sum {α : Type u_1} {ι : Type u_2} {M : Type u_8} [add_comm_monoid M] (s : finset ι) (f : ι M) (a : α) :
finsupp.single a (s.sum (λ (b : ι), f b)) = s.sum (λ (b : ι), finsupp.single a (f b))
theorem finsupp.single_sum {α : Type u_1} {ι : Type u_2} {M : Type u_8} {N : Type u_10} [has_zero M] [add_comm_monoid N] (s : ι →₀ M) (f : ι M N) (a : α) :
finsupp.single a (s.sum f) = s.sum (λ (d : ι) (c : M), finsupp.single a (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] [add_comm_monoid M] {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} [add_comm_monoid N] (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] [add_comm_monoid N] {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} [add_comm_monoid N] (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] [add_comm_monoid N] (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] [add_comm_monoid N] {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 β] [add_comm_monoid M] {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] [add_comm_monoid N] {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] [add_comm_monoid N] {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] [add_comm_group G] {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] [add_comm_group G] {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} [add_zero_class M] [add_comm_monoid N] {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} [add_zero_class M] [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} [add_zero_class M] [add_comm_monoid 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.

theorem finsupp.prod_add_index' {α : Type u_1} {M : Type u_8} {N : Type u_10} [add_zero_class M] [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} [add_zero_class M] [add_comm_monoid N] {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} [add_zero_class M] [comm_monoid N] {f g : α →₀ M} (h : α multiplicative M →* N) :
(f + g).prod (λ (a : α) (b : M), (h a) (multiplicative.of_add b)) = f.prod (λ (a : α) (b : M), (h a) (multiplicative.of_add b)) * g.prod (λ (a : α) (b : M), (h a) (multiplicative.of_add b))
noncomputable def finsupp.lift_add_hom {α : Type u_1} {M : Type u_8} {N : Type u_10} [add_zero_class M] [add_comm_monoid N] :
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} [add_comm_monoid M] [add_comm_monoid N] (F : α M →+ N) (f : α →₀ M) :
(finsupp.lift_add_hom F) f = f.sum (λ (x : α), (F x))
@[simp]
theorem finsupp.lift_add_hom_symm_apply {α : Type u_1} {M : Type u_8} {N : Type u_10} [add_comm_monoid M] [add_comm_monoid N] (F : →₀ M) →+ N) (x : α) :
theorem finsupp.lift_add_hom_symm_apply_apply {α : Type u_1} {M : Type u_8} {N : Type u_10} [add_comm_monoid M] [add_comm_monoid N] (F : →₀ M) →+ N) (x : α) (y : M) :
@[simp]
theorem finsupp.sum_single {α : Type u_1} {M : Type u_8} [add_comm_monoid M] (f : α →₀ M) :
@[simp]
theorem finsupp.sum_univ_single {α : Type u_1} {M : Type u_8} [add_comm_monoid M] [fintype α] (i : α) (m : M) :
finset.univ.sum (λ (j : α), (finsupp.single i m) j) = m
@[simp]
theorem finsupp.sum_univ_single' {α : Type u_1} {M : Type u_8} [add_comm_monoid M] [fintype α] (i : α) (m : M) :
finset.univ.sum (λ (j : α), (finsupp.single j m) i) = m
@[simp]
theorem finsupp.lift_add_hom_apply_single {α : Type u_1} {M : Type u_8} {N : Type u_10} [add_comm_monoid M] [add_comm_monoid N] (f : α M →+ N) (a : α) (b : M) :
@[simp]
theorem finsupp.lift_add_hom_comp_single {α : Type u_1} {M : Type u_8} {N : Type u_10} [add_comm_monoid M] [add_comm_monoid N] (f : α M →+ N) (a : α) :
theorem finsupp.comp_lift_add_hom {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] (g : N →+ P) (f : α M →+ N) :
theorem finsupp.sum_sub_index {α : Type u_1} {γ : Type u_3} {β : Type u_7} [add_comm_group β] [add_comm_group γ] {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] [add_comm_monoid N] {v : α →₀ M} {f : α β} {g : β M N} :
(finsupp.emb_domain f 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} :
(finsupp.emb_domain f 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} [add_comm_monoid M] [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} [add_comm_monoid M] [add_comm_monoid 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₂) :
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} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid 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 (λ (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} [add_comm_monoid M] [add_comm_monoid N] [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} [add_comm_monoid M] [add_comm_monoid 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 (λ (g : α →₀ M), g.sum h) f).sum
theorem finsupp.support_sum_eq_bUnion {α : Type u_1} {ι : Type u_2} {M : Type u_3} [add_comm_monoid M] {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 multiset β} :
multiset.map m (f.sum h) = f.sum (λ (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} [has_zero M] [add_comm_monoid N] {f : α →₀ M} {h : α M multiset N} :
(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} [add_comm_monoid M] {f1 f2 : α →₀ M} (hd : disjoint f1.support f2.support) {β : Type u_2} [add_comm_monoid β] (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} [add_comm_monoid M] {f1 f2 : α →₀ M} (hd : disjoint f1.support 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} [add_comm_monoid M] [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 finset.sum_apply' {α : Type u_1} {ι : Type u_2} {A : Type u_4} [add_comm_monoid A] {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} [add_comm_monoid A] [add_comm_monoid B] (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} [add_comm_monoid A] [add_comm_monoid 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} :
(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} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] (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} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] (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).