Documentation

Mathlib.Algebra.BigOperators.Finsupp.Basic

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.prod {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] (f : α →₀ M) (g : αMN) :
N

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

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

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

    Equations
    Instances For
      theorem Finsupp.prod_of_support_subset {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] (f : α →₀ M) {s : Finset α} (hs : f.support s) (g : αMN) (h : is, g i 0 = 1) :
      f.prod g = xs, g x (f x)
      theorem Finsupp.sum_of_support_subset {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] (f : α →₀ M) {s : Finset α} (hs : f.support s) (g : αMN) (h : is, g i 0 = 0) :
      f.sum g = xs, g x (f x)
      theorem Finsupp.prod_fintype {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] [Fintype α] (f : α →₀ M) (g : αMN) (h : ∀ (i : α), g i 0 = 1) :
      f.prod g = i : α, g i (f i)
      theorem Finsupp.sum_fintype {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] [Fintype α] (f : α →₀ M) (g : αMN) (h : ∀ (i : α), g i 0 = 0) :
      f.sum g = i : α, g i (f i)
      @[simp]
      theorem Finsupp.prod_single_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {a : α} {b : M} {h : αMN} (h_zero : h a 0 = 1) :
      (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} [Zero M] [AddCommMonoid N] {a : α} {b : M} {h : αMN} (h_zero : h a 0 = 0) :
      (single a b).sum h = h a 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'] [CommMonoid N] {f : MM'} {hf : f 0 = 0} {g : α →₀ M} {h : αM'N} (h0 : ∀ (a : α), h a 0 = 1) :
      (mapRange f hf g).prod h = g.prod fun (a : α) (b : M) => h a (f 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'] [AddCommMonoid N] {f : MM'} {hf : f 0 = 0} {g : α →₀ M} {h : αM'N} (h0 : ∀ (a : α), h a 0 = 0) :
      (mapRange f hf g).sum h = g.sum fun (a : α) (b : M) => h a (f b)
      @[simp]
      theorem Finsupp.prod_zero_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {h : αMN} :
      prod 0 h = 1
      @[simp]
      theorem Finsupp.sum_zero_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {h : αMN} :
      sum 0 h = 0
      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'] [CommMonoid N] (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'
      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'] [AddCommMonoid N] (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'
      @[simp]
      theorem Finsupp.prod_ite_eq {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] [DecidableEq α] (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
      @[simp]
      theorem Finsupp.sum_ite_eq {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] [DecidableEq α] (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
      theorem Finsupp.sum_ite_self_eq {α : Type u_1} [DecidableEq α] {N : Type u_16} [AddCommMonoid N] (f : α →₀ N) (a : α) :
      (f.sum fun (x : α) (v : N) => if a = x then v else 0) = f a
      @[simp]
      theorem Finsupp.if_mem_support {α : Type u_1} [DecidableEq α] {N : Type u_16} [Zero N] (f : α →₀ N) (a : α) :
      (if a f.support then f a else 0) = f a

      The left hand side of sum_ite_self_eq simplifies; this is the variant that is useful for simp.

      @[simp]
      theorem Finsupp.prod_ite_eq' {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] [DecidableEq α] (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.

      @[simp]
      theorem Finsupp.sum_ite_eq' {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] [DecidableEq α] (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.

      theorem Finsupp.sum_ite_self_eq' {α : Type u_1} [DecidableEq α] {N : Type u_16} [AddCommMonoid N] (f : α →₀ N) (a : α) :
      (f.sum fun (x : α) (v : N) => if x = a then v else 0) = f a

      A restatement of sum_ite_self_eq with the equality test reversed.

      @[simp]
      theorem Finsupp.prod_pow {α : Type u_1} {N : Type u_10} [CommMonoid N] [Fintype α] (f : α →₀ ) (g : αN) :
      (f.prod fun (a : α) (b : ) => g a ^ b) = a : α, g a ^ f a
      @[simp]
      theorem Finsupp.sum_nsmul {α : Type u_1} {N : Type u_10} [AddCommMonoid N] [Fintype α] (f : α →₀ ) (g : αN) :
      (f.sum fun (a : α) (b : ) => b g a) = a : α, f a g a
      @[simp]
      theorem Finsupp.prod_zpow {α : Type u_1} {N : Type u_16} [DivisionCommMonoid N] [Fintype α] (f : α →₀ ) (g : αN) :
      (f.prod fun (a : α) (b : ) => g a ^ b) = a : α, g a ^ f a
      @[simp]
      theorem Finsupp.sum_zsmul {α : Type u_1} {N : Type u_16} [SubtractionCommMonoid N] [Fintype α] (f : α →₀ ) (g : αN) :
      (f.sum fun (a : α) (b : ) => b g a) = a : α, f a g a
      theorem Finsupp.onFinset_prod {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {s : Finset α} {f : αM} {g : αMN} (hf : ∀ (a : α), f a 0a s) (hg : ∀ (a : α), g a 0 = 1) :
      (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.onFinset_sum {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {s : Finset α} {f : αM} {g : αMN} (hf : ∀ (a : α), f a 0a s) (hg : ∀ (a : α), g a 0 = 0) :
      (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.mul_prod_erase {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] (f : α →₀ M) (y : α) (g : αMN) (hyf : y f.support) :
      g y (f y) * (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} [Zero M] [AddCommMonoid N] (f : α →₀ M) (y : α) (g : αMN) (hyf : y f.support) :
      g y (f y) + (erase y f).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] [CommMonoid N] (f : α →₀ M) (y : α) (g : αMN) (hg : ∀ (i : α), g i 0 = 1) :
      g y (f y) * (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} [Zero M] [AddCommMonoid N] (f : α →₀ M) (y : α) (g : αMN) (hg : ∀ (i : α), g i 0 = 0) :
      g y (f y) + (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 SubmonoidClass.finsupp_prod_mem {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {S : Type u_16} [SetLike S N] [SubmonoidClass S N] (s : S) (f : α →₀ M) (g : αMN) (h : ∀ (c : α), f c 0g c (f c) s) :
      f.prod g s
      theorem AddSubmonoidClass.finsupp_sum_mem {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {S : Type u_16} [SetLike S N] [AddSubmonoidClass S N] (s : S) (f : α →₀ M) (g : αMN) (h : ∀ (c : α), f c 0g c (f c) s) :
      f.sum g s
      theorem Finsupp.prod_congr {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {f : α →₀ M} {g1 g2 : αMN} (h : xf.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} [Zero M] [AddCommMonoid N] {f : α →₀ M} {g1 g2 : αMN} (h : xf.support, g1 x (f x) = g2 x (f x)) :
      f.sum g1 = f.sum g2
      theorem Finsupp.prod_eq_single {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {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)
      theorem Finsupp.sum_eq_single {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {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)
      @[simp]
      theorem Finsupp.prod_eq_zero_iff {α : Type u_1} {ι : Type u_2} {β : Type u_7} [Zero α] [CommMonoidWithZero β] [Nontrivial β] [NoZeroDivisors β] {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 α] [CommMonoidWithZero β] [Nontrivial β] [NoZeroDivisors β] {f : ι →₀ α} {g : ιαβ} :
      f.prod g 0 if.support, g i (f i) 0
      theorem map_finsupp_prod {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [Zero M] [CommMonoid N] [CommMonoid P] {H : Type u_16} [FunLike H N P] [MonoidHomClass H N P] (h : H) (f : α →₀ M) (g : αMN) :
      h (f.prod g) = f.prod fun (a : α) (b : M) => h (g a b)
      theorem map_finsupp_sum {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [Zero M] [AddCommMonoid N] [AddCommMonoid P] {H : Type u_16} [FunLike H N P] [AddMonoidHomClass H N P] (h : H) (f : α →₀ M) (g : αMN) :
      h (f.sum g) = f.sum fun (a : α) (b : M) => h (g a b)
      theorem MonoidHom.coe_finsupp_prod {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [Zero β] [MulOneClass N] [CommMonoid P] (f : α →₀ β) (g : αβN →* P) :
      (f.prod g) = f.prod fun (i : α) (fi : β) => (g i fi)
      theorem AddMonoidHom.coe_finsupp_sum {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [Zero β] [AddZeroClass N] [AddCommMonoid P] (f : α →₀ β) (g : αβN →+ P) :
      (f.sum g) = f.sum fun (i : α) (fi : β) => (g i fi)
      @[simp]
      theorem MonoidHom.finsupp_prod_apply {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [Zero β] [MulOneClass N] [CommMonoid P] (f : α →₀ β) (g : αβN →* P) (x : N) :
      (f.prod g) x = f.prod fun (i : α) (fi : β) => (g i fi) x
      @[simp]
      theorem AddMonoidHom.finsupp_sum_apply {α : Type u_1} {β : Type u_7} {N : Type u_10} {P : Type u_11} [Zero β] [AddZeroClass N] [AddCommMonoid P] (f : α →₀ β) (g : αβN →+ P) (x : N) :
      (f.sum g) x = f.sum fun (i : α) (fi : β) => (g i fi) x
      theorem Finsupp.single_multiset_sum {α : Type u_1} {M : Type u_8} [AddCommMonoid M] (s : Multiset M) (a : α) :
      theorem Finsupp.single_finset_sum {α : Type u_1} {ι : Type u_2} {M : Type u_8} [AddCommMonoid M] (s : Finset ι) (f : ιM) (a : α) :
      single a (∑ bs, f b) = bs, single a (f b)
      theorem Finsupp.single_sum {α : Type u_1} {ι : Type u_2} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] (s : ι →₀ M) (f : ιMN) (a : α) :
      single a (s.sum f) = s.sum fun (d : ι) (c : M) => single a (f d c)
      theorem Finsupp.prod_neg_index {α : Type u_1} {M : Type u_8} {G : Type u_12} [SubtractionMonoid G] [CommMonoid M] {g : α →₀ G} {h : αGM} (h0 : ∀ (a : α), h a 0 = 1) :
      (-g).prod h = g.prod fun (a : α) (b : G) => h a (-b)
      theorem Finsupp.sum_neg_index {α : Type u_1} {M : Type u_8} {G : Type u_12} [SubtractionMonoid G] [AddCommMonoid M] {g : α →₀ G} {h : αGM} (h0 : ∀ (a : α), h a 0 = 0) :
      (-g).sum h = g.sum fun (a : α) (b : G) => h a (-b)
      theorem Finsupp.finset_sum_apply {α : Type u_1} {ι : Type u_2} {N : Type u_10} [AddCommMonoid N] (S : Finset ι) (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] [AddCommMonoid N] {f : α →₀ M} {g : αMβ →₀ N} {a₂ : β} :
      (f.sum g) a₂ = f.sum fun (a₁ : α) (b : M) => (g a₁ b) a₂
      @[simp]
      theorem Finsupp.coe_finset_sum {α : Type u_1} {ι : Type u_2} {N : Type u_10} [AddCommMonoid N] (S : Finset ι) (f : ια →₀ N) :
      (∑ iS, f i) = iS, (f i)
      @[simp]
      theorem Finsupp.coe_sum {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] (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} [DecidableEq β] [Zero M] [AddCommMonoid N] {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} [DecidableEq β] [AddCommMonoid M] {s : Finset α} {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] [AddCommMonoid N] {f : α →₀ M} :
      (f.sum fun (x : α) (x : M) => 0) = 0
      @[simp]
      theorem Finsupp.prod_mul {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {f : α →₀ M} {h₁ h₂ : αMN} :
      (f.prod fun (a : α) (b : M) => h₁ a b * h₂ a b) = f.prod h₁ * f.prod h₂
      @[simp]
      theorem Finsupp.sum_add {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {f : α →₀ M} {h₁ h₂ : αMN} :
      (f.sum fun (a : α) (b : M) => h₁ a b + h₂ a b) = f.sum h₁ + f.sum h₂
      @[simp]
      theorem Finsupp.prod_inv {α : Type u_1} {M : Type u_8} {G : Type u_12} [Zero M] [CommGroup G] {f : α →₀ M} {h : αMG} :
      (f.prod fun (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} [Zero M] [AddCommGroup G] {f : α →₀ M} {h : αMG} :
      (f.sum fun (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} [Zero M] [SubtractionCommMonoid G] {f : α →₀ M} {h₁ h₂ : αMG} :
      (f.sum fun (a : α) (b : M) => h₁ a b - h₂ a b) = f.sum h₁ - f.sum h₂
      theorem Finsupp.prod_add_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [DecidableEq α] [AddZeroClass M] [CommMonoid N] {f 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} [DecidableEq α] [AddZeroClass M] [AddCommMonoid N] {f 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} [AddZeroClass M] [CommMonoid N] {f 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.

      theorem Finsupp.sum_add_index' {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [AddCommMonoid N] {f 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.

      @[simp]
      theorem Finsupp.sum_hom_add_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [AddCommMonoid N] {f 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} [AddZeroClass M] [CommMonoid N] {f g : α →₀ M} (h : αMultiplicative M →* N) :
      ((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} [AddZeroClass M] [AddCommMonoid N] :
      (α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} [AddZeroClass M] [AddCommMonoid N] (F : αM →+ N) (f : α →₀ M) :
        (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} [AddZeroClass M] [AddCommMonoid N] (F : (α →₀ M) →+ N) (x : α) :
        theorem Finsupp.liftAddHom_symm_apply_apply {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [AddCommMonoid N] (F : (α →₀ M) →+ N) (x : α) (y : M) :
        (liftAddHom.symm F x) y = F (single x y)
        @[simp]
        theorem Finsupp.sum_single {α : Type u_1} {M : Type u_8} [AddCommMonoid M] (f : α →₀ M) :
        @[simp]
        theorem Finsupp.univ_sum_single {α : Type u_1} {M : Type u_8} [Fintype α] [AddCommMonoid M] (f : α →₀ M) :
        a : α, 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} [AddCommMonoid M] [Fintype α] (i : α) (m : M) :
        j : α, (single i m) j = m
        @[simp]
        theorem Finsupp.univ_sum_single_apply' {α : Type u_1} {M : Type u_8} [AddCommMonoid M] [Fintype α] (i : α) (m : M) :
        j : α, (single j m) i = m
        theorem Finsupp.equivFunOnFinite_symm_eq_sum {α : Type u_1} {M : Type u_8} [Fintype α] [AddCommMonoid M] (f : αM) :
        equivFunOnFinite.symm f = a : α, single a (f a)
        theorem Finsupp.liftAddHom_apply_single {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [AddCommMonoid N] (f : αM →+ N) (a : α) (b : M) :
        (liftAddHom f) (single a b) = (f a) b
        @[simp]
        theorem Finsupp.liftAddHom_comp_single {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddZeroClass M] [AddCommMonoid N] (f : αM →+ N) (a : α) :
        theorem Finsupp.comp_liftAddHom {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [AddZeroClass M] [AddCommMonoid N] [AddCommMonoid P] (g : N →+ P) (f : αM →+ N) :
        g.comp (liftAddHom f) = liftAddHom fun (a : α) => g.comp (f a)
        theorem Finsupp.sum_sub_index {α : Type u_1} {γ : Type u_3} {β : Type u_7} [AddGroup β] [AddCommGroup γ] {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.prod_embDomain {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {v : α →₀ M} {f : α β} {g : βMN} :
        (embDomain f v).prod g = v.prod fun (a : α) (b : M) => g (f a) b
        theorem Finsupp.sum_embDomain {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {v : α →₀ M} {f : α β} {g : βMN} :
        (embDomain f v).sum g = v.sum fun (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} [AddCommMonoid M] [CommMonoid N] {s : Finset ι} {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_finset_sum_index {α : Type u_1} {ι : Type u_2} {M : Type u_8} {N : Type u_10} [AddCommMonoid M] [AddCommMonoid N] {s : Finset ι} {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_sum_index {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} {P : Type u_11} [Zero M] [AddCommMonoid N] [CommMonoid P] {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.sum_sum_index {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} {P : Type u_11} [Zero M] [AddCommMonoid N] [AddCommMonoid P] {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.multiset_sum_sum_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [AddCommMonoid M] [AddCommMonoid N] (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} [DecidableEq α] [AddCommMonoid M] {g : ια →₀ M} (s : Finset ι) (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 : αMMultiset β} :
        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] [AddCommMonoid N] {f : α →₀ M} {h : αMMultiset N} :
        (f.sum h).sum = f.sum fun (a : α) (b : M) => (h a b).sum
        theorem Finsupp.prod_add_index_of_disjoint {α : Type u_1} {M : Type u_8} [AddCommMonoid M] {f1 f2 : α →₀ M} (hd : Disjoint f1.support f2.support) {β : Type u_16} [CommMonoid β] (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.sum_add_index_of_disjoint {α : Type u_1} {M : Type u_8} [AddCommMonoid M] {f1 f2 : α →₀ M} (hd : Disjoint f1.support f2.support) {β : Type u_16} [AddCommMonoid β] (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_dvd_prod_of_subset_of_dvd {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {f1 f2 : α →₀ M} {g1 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} [AddCommMonoid M] {s : Finset α} (f : (a : α) → a sM) :
        indicator s f = xs.attach, single (↑x) (f x )
        theorem Finsupp.indicator_eq_sum_single {α : Type u_1} {M : Type u_8} [AddCommMonoid M] (s : Finset α) (f : αM) :
        (indicator s fun (x : α) (x_1 : x s) => f x) = xs, single 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] [CommMonoid N] {s : Finset α} (f : (a : α) → a sM) {h : αMN} (h_zero : as, h a 0 = 1) :
        (indicator s f).prod h = xs.attach, h (↑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] [AddCommMonoid N] {s : Finset α} (f : (a : α) → a sM) {h : αMN} (h_zero : as, h a 0 = 0) :
        (indicator s f).sum h = xs.attach, h (↑x) (f x )
        @[simp]
        theorem Finsupp.prod_indicator_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {s : Finset α} (f : αM) {h : αMN} (h_zero : as, h a 0 = 1) :
        (indicator s fun (x : α) (x_1 : x s) => f x).prod h = xs, h x (f x)
        @[simp]
        theorem Finsupp.sum_indicator_index {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {s : Finset α} (f : αM) {h : αMN} (h_zero : as, h a 0 = 0) :
        (indicator s fun (x : α) (x_1 : x s) => f x).sum h = xs, h x (f x)
        theorem Finsupp.prod_mul_eq_prod_mul_of_exists {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [CommMonoid N] {f : α →₀ M} {g : αMN} {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 Finsupp.sum_add_eq_sum_add_of_exists {α : Type u_1} {M : Type u_8} {N : Type u_10} [Zero M] [AddCommMonoid N] {f : α →₀ M} {g : αMN} {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 Finset.sum_apply' {α : Type u_1} {ι : Type u_2} {A : Type u_4} [AddCommMonoid A] {s : Finset α} {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} [AddCommMonoid A] [AddCommMonoid B] (g : ι →₀ A) (k : ιAγB) (x : γ) :
        g.sum k x = g.sum fun (i : ι) (b : A) => k i b x
        theorem Finsupp.sum_apply'' {ι : Type u_2} {γ : Type u_3} {B : Type u_5} [AddCommMonoid B] {A : Type u_16} {F : Type u_17} [AddZeroClass A] [AddCommMonoid F] [FunLike F γ B] (g : ι →₀ A) (k : ιAF) (x : γ) (hg0 : ∀ (i : ι), k i 0 = 0) (hgadd : ∀ (i : ι) (a₁ a₂ : A), k i (a₁ + a₂) = k i a₁ + k i a₂) (h0 : 0 x = 0) (hadd : ∀ (f g : F), (f + g) x = f x + g x) :
        (g.sum k) x = g.sum fun (i : ι) (a : A) => (k i a) x

        Version of Finsupp.apply' that applies in large generality to linear combinations of functions in any FunLike type on which addition is defined pointwise.

        At the time of writing Mathlib does not have a typeclass to express the condition that addition on a FunLike type is pointwise; hence this is asserted via explicit hypotheses.

        theorem Finsupp.sum_sum_index' {α : Type u_1} {ι : Type u_2} {A : Type u_4} {C : Type u_6} [AddCommMonoid A] [AddCommMonoid C] {t : ιAC} {s : Finset α} {f : αι →₀ A} (h0 : ∀ (i : ι), t i 0 = 0) (h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y) :
        (∑ 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} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (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} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (b : S) (s : α →₀ R) {f : αRS} :
        b * s.sum f = s.sum fun (a : α) (c : R) => b * f a c
        @[simp]
        theorem Multiset.card_finsuppSum {α : Type u_1} {ι : Type u_2} {M : Type u_8} [Zero M] (f : ι →₀ M) (g : ιMMultiset α) :
        (f.sum g).card = f.sum fun (i : ι) (m : M) => (g i m).card
        theorem Nat.prod_pow_pos_of_zero_not_mem_support {f : →₀ } (nhf : 0f.support) :
        0 < f.prod fun (x1 x2 : ) => x1 ^ x2

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