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.
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} :
@[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} :
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) :
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) :
@[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) :
@[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) :
@[simp]
theorem
finsupp.sum_ite_self_eq
{α : Type u_1}
[decidable_eq α]
{N : Type u_2}
[add_comm_monoid N]
(f : α →₀ N)
(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) :
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) :
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 : α) :
@[simp]
theorem
finsupp.prod_pow
{α : Type u_1}
{N : Type u_10}
[comm_monoid N]
[fintype α]
(f : α →₀ ℕ)
(g : α → N) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
@[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) :
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) :
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) :
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) :
Deprecated, use _root_.map_finsupp_prod 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) :
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) :
@[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) :
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
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.finset_sum_apply
{α : Type u_1}
{ι : Type u_2}
{N : Type u_10}
[add_comm_monoid N]
(S : finset ι)
(f : ι → α →₀ N)
(a : α) :
theorem
finsupp.coe_finset_sum
{α : Type u_1}
{ι : Type u_2}
{N : Type u_10}
[add_comm_monoid N]
(S : finset ι)
(f : ι → α →₀ N) :
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} :
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} :
@[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} :
@[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} :
@[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} :
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₂) :
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₂) :
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₂) :
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₂) :
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) :
@[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] :
The canonical isomorphism between families of additive monoid homomorphisms α → (M →+ N)
and monoid homomorphisms (α →₀ M) →+ N.
@[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) :
@[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)
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)
@[simp]
@[simp]
theorem
finsupp.sum_single
{α : Type u_1}
{M : Type u_8}
[add_comm_monoid M]
(f : α →₀ M) :
f.sum finsupp.single = f
@[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) :
⇑(⇑finsupp.lift_add_hom f) (finsupp.single a b) = ⇑(f a) b
@[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
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))
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₂) :
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₂) :
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₂) :
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₂) :
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₂) :
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₂) :
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.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 → β) :
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 → β) :
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
finset.sum_apply'
{α : Type u_1}
{ι : Type u_2}
{A : Type u_4}
[add_comm_monoid A]
{s : finset α}
{f : α → ι →₀ A}
(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 : γ) :
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} :
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} :
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} :
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).