mathlib3 documentation

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.

source
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
source
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
source
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))
source
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))
source
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))
source
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))
source
@[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
source
@[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
source
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))
source
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))
source
@[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
source
@[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
source
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'))
source
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'))
source
@[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
source
@[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
source
@[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
source
@[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.

source
@[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.

source
@[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
source
@[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)
source
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.

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

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

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

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

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

source
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
source
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
source
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
source
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
source
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))
source
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))
source
@[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.

source
@[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.

source
@[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.

source
@[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.

source
@[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.

source
@[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.

source
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))
source
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))
source
@[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)
source
@[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)
source
theorem finsupp.single_multiset_sum {α : Type u_1} {M : Type u_8} [add_comm_monoid M] (s : multiset M) (a : α) :
finsupp.single a s.sum = (multiset.map (finsupp.single a) s).sum
source
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))
source
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))
source
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))
source
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))
source
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)
source
@[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₂)
source
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))
source
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))
source
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)
source
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)
source
@[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
source
@[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₂
source
@[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₂
source
@[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)⁻¹
source
@[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
source
@[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₂
source
theorem finsupp.sum_add_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [decidable_eq α] [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.

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

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

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

source
@[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))
source
@[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))
source
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
source
@[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))
source
@[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 : α) :
⇑(finsupp.lift_add_hom.symm) F x = F.comp (finsupp.single_add_hom x)
source
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) :
⇑(⇑(finsupp.lift_add_hom.symm) F x) y = ⇑F (finsupp.single x y)
source
@[simp]
theorem finsupp.lift_add_hom_single_add_hom {α : Type u_1} {M : Type u_8} [add_comm_monoid M] :
⇑finsupp.lift_add_hom finsupp.single_add_hom = add_monoid_hom.id (α →₀ M)
source
@[simp]
theorem finsupp.sum_single {α : Type u_1} {M : Type u_8} [add_comm_monoid M] (f : α →₀ M) :
f.sum finsupp.single = f
source
@[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
source
@[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
source
@[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) :
⇑(⇑finsupp.lift_add_hom f) (finsupp.single a b) = ⇑(f a) b
source
@[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 : α) :
(⇑finsupp.lift_add_hom f).comp (finsupp.single_add_hom a) = f a
source
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) :
g.comp (⇑finsupp.lift_add_hom f) = ⇑finsupp.lift_add_hom (λ (a : α), g.comp (f a))
source
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
source
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)
source
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)
source
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
source
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
source
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)
source
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)
source
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
source
theorem finsupp.support_sum_eq_bUnion {α : Type u_1} {ι : Type u_2} {M : Type u_3} [decidable_eq α] [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)
source
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))
source
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)
source
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

source
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

source
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
source
theorem finsupp.indicator_eq_sum_single {α : Type u_1} {M : Type u_8} [add_comm_monoid M] (s : finset α) (f : Π (a : α), a ∈ s → M) :
finsupp.indicator s f = s.attach.sum (λ (x : {x // x ∈ s}), finsupp.single ↑x (f ↑x _))
source
@[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) :
(finsupp.indicator s f).prod h = s.attach.prod (λ (x : {x // x ∈ s}), h ↑x (f ↑x _))
source
@[simp]
theorem finsupp.sum_indicator_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [has_zero M] [add_comm_monoid N] {s : finset α} (f : Π (a : α), a ∈ s → M) {h : α → M → N} (h_zero : ∀ (a : α), a ∈ s → h a 0 = 0) :
(finsupp.indicator s f).sum h = s.attach.sum (λ (x : {x // x ∈ s}), h ↑x (f ↑x _))
source
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)
source
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)
source
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)
source
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)
source
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)
source
theorem nat.prod_pow_pos_of_zero_not_mem_support {f : ℕ →₀ ℕ} (hf : 0 ∉ f.support) :
0 < f.prod has_pow.pow

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