Big operators for finsupps #

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

Declarations about Finsupp.sum and Finsupp.prod#

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

def Finsupp.sum {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] (f : α →₀ M) (g : αMN) :
N

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

Equations
• f.sum g = af.support, g a (f a)
Instances For
def Finsupp.prod {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] (f : α →₀ M) (g : αMN) :
N

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

Equations
• f.prod g = af.support, g a (f a)
Instances For
theorem Finsupp.sum_of_support_subset {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] (f : α →₀ M) {s : } (hs : f.support s) (g : αMN) (h : is, g i 0 = 0) :
f.sum g = xs, g x (f x)
theorem Finsupp.prod_of_support_subset {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] (f : α →₀ M) {s : } (hs : f.support s) (g : αMN) (h : is, g i 0 = 1) :
f.prod g = xs, g x (f x)
theorem Finsupp.sum_fintype {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] [] (f : α →₀ M) (g : αMN) (h : ∀ (i : α), g i 0 = 0) :
f.sum g = i : α, g i (f i)
theorem Finsupp.prod_fintype {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] [] (f : α →₀ M) (g : αMN) (h : ∀ (i : α), g i 0 = 1) :
f.prod g = i : α, g i (f i)
@[simp]
theorem Finsupp.sum_single_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] {a : α} {b : M} {h : αMN} (h_zero : h a 0 = 0) :
().sum h = h a b
@[simp]
theorem Finsupp.prod_single_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] {a : α} {b : M} {h : αMN} (h_zero : h a 0 = 1) :
().prod h = h a b
theorem Finsupp.sum_mapRange_index {α : Type u_1} {M : Type u_8} {M' : Type u_9} {N : Type u_10} [Zero M] [Zero M'] [] {f : MM'} {hf : f 0 = 0} {g : α →₀ M} {h : αM'N} (h0 : ∀ (a : α), h a 0 = 0) :
(Finsupp.mapRange f hf g).sum h = g.sum fun (a : α) (b : M) => h a (f b)
theorem Finsupp.prod_mapRange_index {α : Type u_1} {M : Type u_8} {M' : Type u_9} {N : Type u_10} [Zero M] [Zero M'] [] {f : MM'} {hf : f 0 = 0} {g : α →₀ M} {h : αM'N} (h0 : ∀ (a : α), h a 0 = 1) :
(Finsupp.mapRange f hf g).prod h = g.prod fun (a : α) (b : M) => h a (f b)
@[simp]
theorem Finsupp.sum_zero_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] {h : αMN} :
= 0
@[simp]
theorem Finsupp.prod_zero_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] {h : αMN} :
= 1
theorem Finsupp.sum_comm {α : Type u_1} {β : Type u_7} {M : Type u_8} {M' : Type u_9} {N : Type u_10} [Zero M] [Zero M'] [] (f : α →₀ M) (g : β →₀ M') (h : αMβM'N) :
(f.sum fun (x : α) (v : M) => g.sum fun (x' : β) (v' : M') => h x v x' v') = g.sum fun (x' : β) (v' : M') => f.sum fun (x : α) (v : M) => h x v x' v'
theorem Finsupp.prod_comm {α : Type u_1} {β : Type u_7} {M : Type u_8} {M' : Type u_9} {N : Type u_10} [Zero M] [Zero M'] [] (f : α →₀ M) (g : β →₀ M') (h : αMβM'N) :
(f.prod fun (x : α) (v : M) => g.prod fun (x' : β) (v' : M') => h x v x' v') = g.prod fun (x' : β) (v' : M') => f.prod fun (x : α) (v : M) => h x v x' v'
@[simp]
theorem Finsupp.sum_ite_eq {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] [] (f : α →₀ M) (a : α) (b : αMN) :
(f.sum fun (x : α) (v : M) => if a = x then b x v else 0) = if a f.support then b a (f a) else 0
@[simp]
theorem Finsupp.prod_ite_eq {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] [] (f : α →₀ M) (a : α) (b : αMN) :
(f.prod fun (x : α) (v : M) => if a = x then b x v else 1) = if a f.support then b a (f a) else 1
theorem Finsupp.sum_ite_self_eq {α : Type u_1} [] {N : Type u_16} [] (f : α →₀ N) (a : α) :
(f.sum fun (x : α) (v : N) => if a = x then v else 0) = f a
@[simp]
theorem Finsupp.sum_ite_self_eq_aux {α : Type u_1} [] {N : Type u_16} [] (f : α →₀ N) (a : α) :
(if a f.support then f a else 0) = f a
@[simp]
theorem Finsupp.sum_ite_eq' {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] [] (f : α →₀ M) (a : α) (b : αMN) :
(f.sum fun (x : α) (v : M) => if x = a then b x v else 0) = if a f.support then b a (f a) else 0

A restatement of sum_ite_eq with the equality test reversed.

@[simp]
theorem Finsupp.prod_ite_eq' {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] [] (f : α →₀ M) (a : α) (b : αMN) :
(f.prod fun (x : α) (v : M) => if x = a then b x v else 1) = if a f.support then b a (f a) else 1

A restatement of prod_ite_eq with the equality test reversed.

theorem Finsupp.sum_ite_self_eq' {α : Type u_1} [] {N : Type u_16} [] (f : α →₀ N) (a : α) :
(f.sum fun (x : α) (v : N) => if x = a then v else 0) = f a
@[simp]
theorem Finsupp.prod_pow {α : Type u_1} {N : Type u_10} [] [] (f : α →₀ ) (g : αN) :
(f.prod fun (a : α) (b : ) => g a ^ b) = a : α, g a ^ f a
theorem Finsupp.onFinset_sum {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] {s : } {f : αM} {g : αMN} (hf : ∀ (a : α), f a 0a s) (hg : ∀ (a : α), g a 0 = 0) :
(Finsupp.onFinset s f hf).sum g = as, g a (f a)

If g maps a second argument of 0 to 0, summing it over the result of onFinset is the same as summing it over the original Finset.

theorem Finsupp.onFinset_prod {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] {s : } {f : αM} {g : αMN} (hf : ∀ (a : α), f a 0a s) (hg : ∀ (a : α), g a 0 = 1) :
(Finsupp.onFinset s f hf).prod g = as, g a (f a)

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

theorem Finsupp.add_sum_erase {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] (f : α →₀ M) (y : α) (g : αMN) (hyf : y f.support) :
g y (f y) + ().sum g = f.sum g

Taking a sum over f : α →₀ M is the same as adding the value on a single element y ∈ f.support to the sum over erase y f.

theorem Finsupp.mul_prod_erase {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] (f : α →₀ M) (y : α) (g : αMN) (hyf : y f.support) :
g y (f y) * ().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} [Zero M] [] (f : α →₀ M) (y : α) (g : αMN) (hg : ∀ (i : α), g i 0 = 0) :
g y (f y) + ().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 Finsupp.mul_prod_erase' {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] (f : α →₀ M) (y : α) (g : αMN) (hg : ∀ (i : α), g i 0 = 1) :
g y (f y) * ().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 AddSubmonoidClass.finsupp_sum_mem {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] {S : Type u_16} [SetLike S N] [] (s : S) (f : α →₀ M) (g : αMN) (h : ∀ (c : α), f c 0g c (f c) s) :
f.sum g s
theorem SubmonoidClass.finsupp_prod_mem {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] {S : Type u_16} [SetLike S N] [] (s : S) (f : α →₀ M) (g : αMN) (h : ∀ (c : α), f c 0g c (f c) s) :
f.prod g s
theorem Finsupp.sum_congr {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] {f : α →₀ M} {g1 : αMN} {g2 : αMN} (h : xf.support, g1 x (f x) = g2 x (f x)) :
f.sum g1 = f.sum g2
theorem Finsupp.prod_congr {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] {f : α →₀ M} {g1 : αMN} {g2 : αMN} (h : xf.support, g1 x (f x) = g2 x (f x)) :
f.prod g1 = f.prod g2
theorem Finsupp.sum_eq_single {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] {f : α →₀ M} (a : α) {g : αMN} (h₀ : ∀ (b : α), f b 0b ag b (f b) = 0) (h₁ : f a = 0g a 0 = 0) :
f.sum g = g a (f a)
theorem Finsupp.prod_eq_single {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] {f : α →₀ M} (a : α) {g : αMN} (h₀ : ∀ (b : α), f b 0b ag b (f b) = 1) (h₁ : f a = 0g a 0 = 1) :
f.prod g = g a (f a)
@[simp]
theorem Finsupp.prod_eq_zero_iff {α : Type u_1} {ι : Type u_2} {β : Type u_7} [Zero α] [] [] {f : ι →₀ α} {g : ιαβ} :
f.prod g = 0 if.support, g i (f i) = 0
theorem Finsupp.prod_ne_zero_iff {α : Type u_1} {ι : Type u_2} {β : Type u_7} [Zero α] [] [] {f : ι →₀ α} {g : ιαβ} :
f.prod g 0 if.support, g i (f i) 0
theorem map_finsupp_sum {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [Zero M] [] [] {H : Type u_16} [FunLike H N P] [] (h : H) (f : α →₀ M) (g : αMN) :
h (f.sum g) = f.sum fun (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} [Zero M] [] [] {H : Type u_16} [FunLike H N P] [] (h : H) (f : α →₀ M) (g : αMN) :
h (f.prod g) = f.prod fun (a : α) (b : M) => h (g a b)
theorem AddMonoidHom.coe_finsupp_sum {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [Zero β] [] [] (f : α →₀ β) (g : αβN →+ P) :
(f.sum g) = f.sum fun (i : α) (fi : β) => (g i fi)
theorem MonoidHom.coe_finsupp_prod {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [Zero β] [] [] (f : α →₀ β) (g : αβN →* P) :
(f.prod g) = f.prod fun (i : α) (fi : β) => (g i fi)
@[simp]
theorem AddMonoidHom.finsupp_sum_apply {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [Zero β] [] [] (f : α →₀ β) (g : αβN →+ P) (x : N) :
(f.sum g) x = f.sum fun (i : α) (fi : β) => (g i fi) x
@[simp]
theorem MonoidHom.finsupp_prod_apply {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [Zero β] [] [] (f : α →₀ β) (g : αβN →* P) (x : N) :
(f.prod g) x = f.prod fun (i : α) (fi : β) => (g i fi) x
theorem Finsupp.single_multiset_sum {α : Type u_1} {M : Type u_8} [] (s : ) (a : α) :
Finsupp.single a s.sum = ().sum
theorem Finsupp.single_finset_sum {α : Type u_1} {ι : Type u_2} {M : Type u_8} [] (s : ) (f : ιM) (a : α) :
Finsupp.single a (bs, f b) = bs, Finsupp.single a (f b)
theorem Finsupp.single_sum {α : Type u_1} {ι : Type u_2} {M : Type u_8} {N : Type u_10} [Zero M] [] (s : ι →₀ M) (f : ιMN) (a : α) :
Finsupp.single a (s.sum f) = s.sum fun (d : ι) (c : M) => Finsupp.single a (f d c)
theorem Finsupp.sum_neg_index {α : Type u_1} {M : Type u_8} {G : Type u_12} [] [] {g : α →₀ G} {h : αGM} (h0 : ∀ (a : α), h a 0 = 0) :
(-g).sum h = g.sum fun (a : α) (b : G) => h a (-b)
theorem Finsupp.prod_neg_index {α : Type u_1} {M : Type u_8} {G : Type u_12} [] [] {g : α →₀ G} {h : αGM} (h0 : ∀ (a : α), h a 0 = 1) :
(-g).prod h = g.prod fun (a : α) (b : G) => h a (-b)
theorem Finsupp.finset_sum_apply {α : Type u_1} {ι : Type u_2} {N : Type u_10} [] (S : ) (f : ια →₀ N) (a : α) :
(iS, f i) a = iS, (f i) a
@[simp]
theorem Finsupp.sum_apply {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [Zero M] [] {f : α →₀ M} {g : αMβ →₀ N} {a₂ : β} :
(f.sum g) a₂ = f.sum fun (a₁ : α) (b : M) => (g a₁ b) a₂
theorem Finsupp.coe_finset_sum {α : Type u_1} {ι : Type u_2} {N : Type u_10} [] (S : ) (f : ια →₀ N) :
(iS, f i) = iS, (f i)
theorem Finsupp.coe_sum {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [Zero M] [] (f : α →₀ M) (g : αMβ →₀ N) :
(f.sum g) = f.sum fun (a₁ : α) (b : M) => (g a₁ b)
theorem Finsupp.support_sum {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [] [Zero M] [] {f : α →₀ M} {g : αMβ →₀ N} :
(f.sum g).support f.support.biUnion fun (a : α) => (g a (f a)).support
theorem Finsupp.support_finset_sum {α : Type u_1} {β : Type u_7} {M : Type u_8} [] [] {s : } {f : αβ →₀ M} :
(s.sum f).support s.biUnion fun (x : α) => (f x).support
@[simp]
theorem Finsupp.sum_zero {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] {f : α →₀ M} :
(f.sum fun (x : α) (x : M) => 0) = 0
@[simp]
theorem Finsupp.sum_add {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] {f : α →₀ M} {h₁ : αMN} {h₂ : αMN} :
(f.sum fun (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} [Zero M] [] {f : α →₀ M} {h₁ : αMN} {h₂ : αMN} :
(f.prod fun (a : α) (b : M) => h₁ a b * h₂ a b) = f.prod h₁ * f.prod h₂
@[simp]
theorem Finsupp.sum_neg {α : Type u_1} {M : Type u_8} {G : Type u_12} [Zero M] [] {f : α →₀ M} {h : αMG} :
(f.sum fun (a : α) (b : M) => -h a b) = -f.sum h
@[simp]
theorem Finsupp.prod_inv {α : Type u_1} {M : Type u_8} {G : Type u_12} [Zero M] [] {f : α →₀ M} {h : αMG} :
(f.prod fun (a : α) (b : M) => (h a b)⁻¹) = (f.prod h)⁻¹
@[simp]
theorem Finsupp.sum_sub {α : Type u_1} {M : Type u_8} {G : Type u_12} [Zero M] [] {f : α →₀ M} {h₁ : αMG} {h₂ : αMG} :
(f.sum fun (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} [] [] [] {f : α →₀ M} {g : α →₀ M} {h : αMN} (h_zero : af.support g.support, h a 0 = 0) (h_add : af.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} [] [] [] {f : α →₀ M} {g : α →₀ M} {h : αMN} (h_zero : af.support g.support, h a 0 = 1) (h_add : af.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 : α →₀ M} {g : α →₀ M} {h : αMN} (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} [] [] {f : α →₀ M} {g : α →₀ M} {h : αMN} (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 : α →₀ M} {g : α →₀ M} (h : αM →+ N) :
((f + g).sum fun (x : α) => (h x)) = (f.sum fun (x : α) => (h x)) + g.sum fun (x : α) => (h x)
@[simp]
theorem Finsupp.prod_hom_add_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [] [] {f : α →₀ M} {g : α →₀ M} (h : α) :
((f + g).prod fun (a : α) (b : M) => (h a) (Multiplicative.ofAdd b)) = (f.prod fun (a : α) (b : M) => (h a) (Multiplicative.ofAdd b)) * g.prod fun (a : α) (b : M) => (h a) (Multiplicative.ofAdd b)
def Finsupp.liftAddHom {α : 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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Finsupp.liftAddHom_apply {α : Type u_1} {M : Type u_8} {N : Type u_10} [] [] (F : αM →+ N) (f : α →₀ M) :
(Finsupp.liftAddHom F) f = f.sum fun (x : α) => (F x)
@[simp]
theorem Finsupp.liftAddHom_symm_apply {α : Type u_1} {M : Type u_8} {N : Type u_10} [] [] (F : (α →₀ M) →+ N) (x : α) :
theorem Finsupp.liftAddHom_symm_apply_apply {α : Type u_1} {M : Type u_8} {N : Type u_10} [] [] (F : (α →₀ M) →+ N) (x : α) (y : M) :
(Finsupp.liftAddHom.symm F x) y = F ()
@[simp]
theorem Finsupp.liftAddHom_singleAddHom {α : Type u_1} {M : Type u_8} [] :
@[simp]
theorem Finsupp.sum_single {α : Type u_1} {M : Type u_8} [] (f : α →₀ M) :
f.sum Finsupp.single = f
@[simp]
theorem Finsupp.univ_sum_single {α : Type u_1} {M : Type u_8} [] [] (f : α →₀ M) :
a : α, Finsupp.single a (f a) = f

The Finsupp version of Finset.univ_sum_single

@[simp]
theorem Finsupp.univ_sum_single_apply {α : Type u_1} {M : Type u_8} [] [] (i : α) (m : M) :
j : α, () j = m
@[simp]
theorem Finsupp.univ_sum_single_apply' {α : Type u_1} {M : Type u_8} [] [] (i : α) (m : M) :
j : α, () i = m
theorem Finsupp.equivFunOnFinite_symm_eq_sum {α : Type u_1} {M : Type u_8} [] [] (f : αM) :
Finsupp.equivFunOnFinite.symm f = a : α, Finsupp.single a (f a)
theorem Finsupp.liftAddHom_apply_single {α : Type u_1} {M : Type u_8} {N : Type u_10} [] [] (f : αM →+ N) (a : α) (b : M) :
(Finsupp.liftAddHom f) () = (f a) b
@[simp]
theorem Finsupp.liftAddHom_comp_single {α : Type u_1} {M : Type u_8} {N : Type u_10} [] [] (f : αM →+ N) (a : α) :
theorem Finsupp.comp_liftAddHom {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [] [] [] (g : N →+ P) (f : αM →+ N) :
g.comp (Finsupp.liftAddHom f) = Finsupp.liftAddHom fun (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_embDomain {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [Zero M] [] {v : α →₀ M} {f : α β} {g : βMN} :
().sum g = v.sum fun (a : α) (b : M) => g (f a) b
theorem Finsupp.prod_embDomain {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [Zero M] [] {v : α →₀ M} {f : α β} {g : βMN} :
().prod g = v.prod fun (a : α) (b : M) => g (f a) b
theorem Finsupp.sum_finset_sum_index {α : Type u_1} {ι : Type u_2} {M : Type u_8} {N : Type u_10} [] [] {s : } {g : ια →₀ M} {h : αMN} (h_zero : ∀ (a : α), h a 0 = 0) (h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) :
is, (g i).sum h = (is, g i).sum h
theorem Finsupp.prod_finset_sum_index {α : Type u_1} {ι : Type u_2} {M : Type u_8} {N : Type u_10} [] [] {s : } {g : ια →₀ M} {h : αMN} (h_zero : ∀ (a : α), h a 0 = 1) (h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂) :
is, (g i).prod h = (is, g i).prod 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 : βNP} (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 fun (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} [] [] [] {f : α →₀ M} {g : αMβ →₀ N} {h : βNP} (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 fun (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 : αMN) (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 (fun (g : α →₀ M) => g.sum h) f).sum
theorem Finsupp.support_sum_eq_biUnion {α : Type u_16} {ι : Type u_17} {M : Type u_18} [] [] {g : ια →₀ M} (s : ) (h : ∀ (i₁ i₂ : ι), i₁ i₂Disjoint (g i₁).support (g i₂).support) :
(is, g i).support = s.biUnion fun (i : ι) => (g i).support
theorem Finsupp.multiset_map_sum {α : Type u_1} {γ : Type u_3} {β : Type u_7} {M : Type u_8} [Zero M] {f : α →₀ M} {m : βγ} {h : αM} :
Multiset.map m (f.sum h) = f.sum fun (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} [Zero M] [] {f : α →₀ M} {h : αM} :
(f.sum h).sum = f.sum fun (a : α) (b : M) => (h a b).sum
theorem Finsupp.sum_add_index_of_disjoint {α : Type u_1} {M : Type u_8} [] {f1 : α →₀ M} {f2 : α →₀ M} (hd : Disjoint f1.support f2.support) {β : Type u_16} [] (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 : α →₀ M} {f2 : α →₀ M} (hd : Disjoint f1.support f2.support) {β : Type u_16} [] (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} [] [] {f1 : α →₀ M} {f2 : α →₀ M} {g1 : αMN} {g2 : αMN} (h1 : f1.support f2.support) (h2 : af1.support, g1 a (f1 a) g2 a (f2 a)) :
f1.prod g1 f2.prod g2
theorem Finsupp.indicator_eq_sum_attach_single {α : Type u_1} {M : Type u_8} [] {s : } (f : (a : α) → a sM) :
= xs.attach, Finsupp.single (x) (f x )
theorem Finsupp.indicator_eq_sum_single {α : Type u_1} {M : Type u_8} [] (s : ) (f : αM) :
(Finsupp.indicator s fun (x : α) (x_1 : x s) => f x) = xs, Finsupp.single x (f x)
@[simp]
theorem Finsupp.sum_indicator_index_eq_sum_attach {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] {s : } (f : (a : α) → a sM) {h : αMN} (h_zero : as, h a 0 = 0) :
().sum h = xs.attach, h (x) (f x )
@[simp]
theorem Finsupp.prod_indicator_index_eq_prod_attach {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] {s : } (f : (a : α) → a sM) {h : αMN} (h_zero : as, h a 0 = 1) :
().prod h = xs.attach, h (x) (f x )
@[simp]
theorem Finsupp.sum_indicator_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] {s : } (f : αM) {h : αMN} (h_zero : as, h a 0 = 0) :
(Finsupp.indicator s fun (x : α) (x_1 : x s) => f x).sum h = xs, h x (f x)
@[simp]
theorem Finsupp.prod_indicator_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [] {s : } (f : αM) {h : αMN} (h_zero : as, h a 0 = 1) :
(Finsupp.indicator s fun (x : α) (x_1 : x s) => f x).prod h = xs, h x (f x)
theorem Finsupp.sum_cons {M : Type u_8} [] (n : ) (σ : Fin n →₀ M) (i : M) :
(().sum fun (x : Fin (n + 1)) (e : M) => e) = i + σ.sum fun (x : Fin n) (e : M) => e
theorem Finsupp.sum_cons' {M : Type u_8} {N : Type u_10} [] [] (n : ) (σ : Fin n →₀ M) (i : M) (f : Fin (n + 1)MN) (h : ∀ (x : Fin (n + 1)), f x 0 = 0) :
().sum f = f 0 i + σ.sum ()
theorem Finsupp.sum_add_eq_sum_add_of_exists {α : Type u_1} {M : Type u_8} {N : Type u_10} [] [Zero M] [] {f : α →₀ M} {g : αMN} {n₁ : N} {n₂ : N} (a : α) (ha : a f.support) (h : g a (f a) + n₁ = g a (f a) + n₂) :
f.sum g + n₁ = f.sum g + n₂
theorem Finsupp.prod_mul_eq_prod_mul_of_exists {α : Type u_1} {M : Type u_8} {N : Type u_10} [] [Zero M] [] {f : α →₀ M} {g : αMN} {n₁ : N} {n₂ : N} (a : α) (ha : a f.support) (h : g a (f a) * n₁ = g a (f a) * n₂) :
f.prod g * n₁ = f.prod g * n₂
theorem Finset.sum_apply' {α : Type u_1} {ι : Type u_2} {A : Type u_4} [] {s : } {f : αι →₀ A} (i : ι) :
(ks, f k) i = ks, (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 fun (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 : ιAC} (h0 : ∀ (i : ι), t i 0 = 0) (h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y) {s : } {f : αι →₀ A} :
(xs, f x).sum t = xs, (f x).sum t
theorem Finsupp.sum_mul {α : Type u_1} {R : Type u_14} {S : Type u_15} (b : S) (s : α →₀ R) {f : αRS} :
s.sum f * b = s.sum fun (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 : αRS} :
b * s.sum f = s.sum fun (a : α) (c : R) => b * f a c
theorem Nat.prod_pow_pos_of_zero_not_mem_support {f : } (nhf : 0f.support) :
0 < f.prod fun (x x_1 : ) => x ^ x_1

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