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 AddMonoid.
def
Finsupp.sum
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
[inst : Zero M]
[inst : AddCommMonoid N]
(f : α →₀ M)
(g : α → M → N)
:
N
sum f g is the sum of g a (f a) over the support of f.
Equations
- Finsupp.sum f g = Finset.sum f.support fun a => g a (↑f a)
def
Finsupp.prod
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
[inst : Zero M]
[inst : CommMonoid N]
(f : α →₀ M)
(g : α → M → N)
:
N
prod f g is the product of g a (f a) over the support of f.
Equations
- Finsupp.prod f g = Finset.prod f.support fun a => g a (↑f a)
theorem
Finsupp.sum_of_support_subset
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
[inst : Zero M]
[inst : AddCommMonoid N]
(f : α →₀ M)
{s : Finset α}
(hs : f.support ⊆ s)
(g : α → M → N)
(h : ∀ (i : α), i ∈ s → g i 0 = 0)
:
Finsupp.sum f g = Finset.sum s fun x => g x (↑f x)
theorem
Finsupp.prod_of_support_subset
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
[inst : Zero M]
[inst : CommMonoid N]
(f : α →₀ M)
{s : Finset α}
(hs : f.support ⊆ s)
(g : α → M → N)
(h : ∀ (i : α), i ∈ s → g i 0 = 1)
:
Finsupp.prod f g = Finset.prod s fun x => g x (↑f x)
theorem
Finsupp.sum_fintype
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
[inst : Zero M]
[inst : AddCommMonoid N]
[inst : Fintype α]
(f : α →₀ M)
(g : α → M → N)
(h : ∀ (i : α), g i 0 = 0)
:
Finsupp.sum f g = Finset.sum Finset.univ fun i => g i (↑f i)
theorem
Finsupp.prod_fintype
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
[inst : Zero M]
[inst : CommMonoid N]
[inst : Fintype α]
(f : α →₀ M)
(g : α → M → N)
(h : ∀ (i : α), g i 0 = 1)
:
Finsupp.prod f g = Finset.prod Finset.univ fun i => g i (↑f i)
@[simp]
theorem
Finsupp.sum_single_index
{α : Type u_3}
{M : Type u_2}
{N : Type u_1}
[inst : Zero M]
[inst : AddCommMonoid N]
{a : α}
{b : M}
{h : α → M → N}
(h_zero : h a 0 = 0)
:
Finsupp.sum (Finsupp.single a b) h = h a b
@[simp]
theorem
Finsupp.prod_single_index
{α : Type u_3}
{M : Type u_2}
{N : Type u_1}
[inst : Zero M]
[inst : CommMonoid N]
{a : α}
{b : M}
{h : α → M → N}
(h_zero : h a 0 = 1)
:
Finsupp.prod (Finsupp.single a b) h = h a b
theorem
Finsupp.sum_mapRange_index
{α : Type u_3}
{M : Type u_2}
{M' : Type u_1}
{N : Type u_4}
[inst : Zero M]
[inst : Zero M']
[inst : AddCommMonoid N]
{f : M → M'}
{hf : f 0 = 0}
{g : α →₀ M}
{h : α → M' → N}
(h0 : ∀ (a : α), h a 0 = 0)
:
Finsupp.sum (Finsupp.mapRange f hf g) h = Finsupp.sum g fun a b => h a (f b)
theorem
Finsupp.prod_mapRange_index
{α : Type u_3}
{M : Type u_2}
{M' : Type u_1}
{N : Type u_4}
[inst : Zero M]
[inst : Zero M']
[inst : CommMonoid N]
{f : M → M'}
{hf : f 0 = 0}
{g : α →₀ M}
{h : α → M' → N}
(h0 : ∀ (a : α), h a 0 = 1)
:
Finsupp.prod (Finsupp.mapRange f hf g) h = Finsupp.prod g fun a b => h a (f b)
@[simp]
theorem
Finsupp.sum_zero_index
{α : Type u_2}
{M : Type u_3}
{N : Type u_1}
[inst : Zero M]
[inst : AddCommMonoid N]
{h : α → M → N}
:
Finsupp.sum 0 h = 0
@[simp]
theorem
Finsupp.prod_zero_index
{α : Type u_2}
{M : Type u_3}
{N : Type u_1}
[inst : Zero M]
[inst : CommMonoid N]
{h : α → M → N}
:
Finsupp.prod 0 h = 1
theorem
Finsupp.sum_comm
{α : Type u_1}
{β : Type u_3}
{M : Type u_2}
{M' : Type u_4}
{N : Type u_5}
[inst : Zero M]
[inst : Zero M']
[inst : AddCommMonoid N]
(f : α →₀ M)
(g : β →₀ M')
(h : α → M → β → M' → N)
:
(Finsupp.sum f fun x v => Finsupp.sum g fun x' v' => h x v x' v') = Finsupp.sum g fun x' v' => Finsupp.sum f fun x v => h x v x' v'
theorem
Finsupp.prod_comm
{α : Type u_1}
{β : Type u_3}
{M : Type u_2}
{M' : Type u_4}
{N : Type u_5}
[inst : Zero M]
[inst : Zero M']
[inst : CommMonoid N]
(f : α →₀ M)
(g : β →₀ M')
(h : α → M → β → M' → N)
:
(Finsupp.prod f fun x v => Finsupp.prod g fun x' v' => h x v x' v') = Finsupp.prod g fun x' v' => Finsupp.prod f fun x v => h x v x' v'
@[simp]
theorem
Finsupp.sum_ite_eq
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
[inst : Zero M]
[inst : AddCommMonoid N]
[inst : DecidableEq α]
(f : α →₀ M)
(a : α)
(b : α → M → N)
:
(Finsupp.sum f fun x v => 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_2}
{N : Type u_3}
[inst : Zero M]
[inst : CommMonoid N]
[inst : DecidableEq α]
(f : α →₀ M)
(a : α)
(b : α → M → N)
:
(Finsupp.prod f fun x v => 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}
[inst : DecidableEq α]
{N : Type u_2}
[inst : AddCommMonoid N]
(f : α →₀ N)
(a : α)
:
(Finsupp.sum f fun x v => if a = x then v else 0) = ↑f a
@[simp]
theorem
Finsupp.sum_ite_self_eq_aux
{α : Type u_1}
[inst : DecidableEq α]
{N : Type u_2}
[inst : AddCommMonoid N]
(f : α →₀ N)
(a : α)
:
@[simp]
theorem
Finsupp.sum_ite_eq'
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
[inst : Zero M]
[inst : AddCommMonoid N]
[inst : DecidableEq α]
(f : α →₀ M)
(a : α)
(b : α → M → N)
:
(Finsupp.sum f fun x v => 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_2}
{N : Type u_3}
[inst : Zero M]
[inst : CommMonoid N]
[inst : DecidableEq α]
(f : α →₀ M)
(a : α)
(b : α → M → N)
:
(Finsupp.prod f fun x v => 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}
[inst : DecidableEq α]
{N : Type u_2}
[inst : AddCommMonoid N]
(f : α →₀ N)
(a : α)
:
(Finsupp.sum f fun x v => if x = a then v else 0) = ↑f a
@[simp]
theorem
Finsupp.prod_pow
{α : Type u_1}
{N : Type u_2}
[inst : CommMonoid N]
[inst : Fintype α]
(f : α →₀ ℕ)
(g : α → N)
:
(Finsupp.prod f fun a b => g a ^ b) = Finset.prod Finset.univ fun a => g a ^ ↑f a
theorem
Finsupp.onFinset_sum
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
[inst : Zero M]
[inst : AddCommMonoid N]
{s : Finset α}
{f : α → M}
{g : α → M → N}
(hf : ∀ (a : α), f a ≠ 0 → a ∈ s)
(hg : ∀ (a : α), g a 0 = 0)
:
Finsupp.sum (Finsupp.onFinset s f hf) g = Finset.sum s fun a => 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_2}
{N : Type u_3}
[inst : Zero M]
[inst : CommMonoid N]
{s : Finset α}
{f : α → M}
{g : α → M → N}
(hf : ∀ (a : α), f a ≠ 0 → a ∈ s)
(hg : ∀ (a : α), g a 0 = 1)
:
Finsupp.prod (Finsupp.onFinset s f hf) g = Finset.prod s fun a => 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_2}
{N : Type u_3}
[inst : Zero M]
[inst : AddCommMonoid N]
(f : α →₀ M)
(y : α)
(g : α → M → N)
(hyf : y ∈ f.support)
:
g y (↑f y) + Finsupp.sum (Finsupp.erase y f) g = Finsupp.sum f g
Taking a sum over over f : α →₀ M is the same as adding the value on a
single element y ∈ f.support to the sum over erase y f.
theorem
Finsupp.mul_prod_erase
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
[inst : Zero M]
[inst : CommMonoid N]
(f : α →₀ M)
(y : α)
(g : α → M → N)
(hyf : y ∈ f.support)
:
g y (↑f y) * Finsupp.prod (Finsupp.erase y f) g = Finsupp.prod f 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_2}
{N : Type u_3}
[inst : Zero M]
[inst : AddCommMonoid N]
(f : α →₀ M)
(y : α)
(g : α → M → N)
(hg : ∀ (i : α), g i 0 = 0)
:
g y (↑f y) + Finsupp.sum (Finsupp.erase y f) g = Finsupp.sum f 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_2}
{N : Type u_3}
[inst : Zero M]
[inst : CommMonoid N]
(f : α →₀ M)
(y : α)
(g : α → M → N)
(hg : ∀ (i : α), g i 0 = 1)
:
g y (↑f y) * Finsupp.prod (Finsupp.erase y f) g = Finsupp.prod f 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_3}
{M : Type u_4}
{N : Type u_2}
[inst : Zero M]
[inst : AddCommMonoid N]
{S : Type u_1}
[inst : SetLike S N]
[inst : AddSubmonoidClass S N]
(s : S)
(f : α →₀ M)
(g : α → M → N)
(h : ∀ (c : α), ↑f c ≠ 0 → g c (↑f c) ∈ s)
:
Finsupp.sum f g ∈ s
theorem
SubmonoidClass.finsupp_prod_mem
{α : Type u_3}
{M : Type u_4}
{N : Type u_2}
[inst : Zero M]
[inst : CommMonoid N]
{S : Type u_1}
[inst : SetLike S N]
[inst : SubmonoidClass S N]
(s : S)
(f : α →₀ M)
(g : α → M → N)
(h : ∀ (c : α), ↑f c ≠ 0 → g c (↑f c) ∈ s)
:
Finsupp.prod f g ∈ s
theorem
Finsupp.sum_congr
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
[inst : Zero M]
[inst : AddCommMonoid N]
{f : α →₀ M}
{g1 : α → M → N}
{g2 : α → M → N}
(h : ∀ (x : α), x ∈ f.support → g1 x (↑f x) = g2 x (↑f x))
:
Finsupp.sum f g1 = Finsupp.sum f g2
theorem
Finsupp.prod_congr
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
[inst : Zero M]
[inst : CommMonoid N]
{f : α →₀ M}
{g1 : α → M → N}
{g2 : α → M → N}
(h : ∀ (x : α), x ∈ f.support → g1 x (↑f x) = g2 x (↑f x))
:
Finsupp.prod f g1 = Finsupp.prod f g2
theorem
map_finsupp_sum
{α : Type u_5}
{M : Type u_1}
{N : Type u_2}
{P : Type u_3}
[inst : Zero M]
[inst : AddCommMonoid N]
[inst : AddCommMonoid P]
{H : Type u_4}
[inst : AddMonoidHomClass H N P]
(h : H)
(f : α →₀ M)
(g : α → M → N)
:
↑h (Finsupp.sum f g) = Finsupp.sum f fun a b => ↑h (g a b)
theorem
map_finsupp_prod
{α : Type u_5}
{M : Type u_1}
{N : Type u_2}
{P : Type u_3}
[inst : Zero M]
[inst : CommMonoid N]
[inst : CommMonoid P]
{H : Type u_4}
[inst : MonoidHomClass H N P]
(h : H)
(f : α →₀ M)
(g : α → M → N)
:
↑h (Finsupp.prod f g) = Finsupp.prod f fun a b => ↑h (g a b)
theorem
AddEquiv.map_finsupp_sum
{α : Type u_4}
{M : Type u_1}
{N : Type u_2}
{P : Type u_3}
[inst : Zero M]
[inst : AddCommMonoid N]
[inst : AddCommMonoid P]
(h : N ≃+ P)
(f : α →₀ M)
(g : α → M → N)
:
↑h (Finsupp.sum f g) = Finsupp.sum f fun a b => ↑h (g a b)
Deprecated, use _root_.map_finsupp_sum instead.
theorem
MulEquiv.map_finsupp_prod
{α : Type u_4}
{M : Type u_1}
{N : Type u_2}
{P : Type u_3}
[inst : Zero M]
[inst : CommMonoid N]
[inst : CommMonoid P]
(h : N ≃* P)
(f : α →₀ M)
(g : α → M → N)
:
↑h (Finsupp.prod f g) = Finsupp.prod f fun a b => ↑h (g a b)
Deprecated, use _root_.map_finsupp_prod instead.
theorem
AddMonoidHom.map_finsupp_sum
{α : Type u_4}
{M : Type u_1}
{N : Type u_2}
{P : Type u_3}
[inst : Zero M]
[inst : AddCommMonoid N]
[inst : AddCommMonoid P]
(h : N →+ P)
(f : α →₀ M)
(g : α → M → N)
:
↑h (Finsupp.sum f g) = Finsupp.sum f fun a b => ↑h (g a b)
Deprecated, use _root_.map_finsupp_sum instead.
theorem
MonoidHom.map_finsupp_prod
{α : Type u_4}
{M : Type u_1}
{N : Type u_2}
{P : Type u_3}
[inst : Zero M]
[inst : CommMonoid N]
[inst : CommMonoid P]
(h : N →* P)
(f : α →₀ M)
(g : α → M → N)
:
↑h (Finsupp.prod f g) = Finsupp.prod f fun a b => ↑h (g a b)
Deprecated, use _root_.map_finsupp_prod instead.
theorem
RingHom.map_finsupp_sum
{α : Type u_4}
{M : Type u_1}
{R : Type u_2}
{S : Type u_3}
[inst : Zero M]
[inst : Semiring R]
[inst : Semiring S]
(h : R →+* S)
(f : α →₀ M)
(g : α → M → R)
:
↑h (Finsupp.sum f g) = Finsupp.sum f fun a b => ↑h (g a b)
Deprecated, use _root_.map_finsupp_sum instead.
theorem
RingHom.map_finsupp_prod
{α : Type u_4}
{M : Type u_1}
{R : Type u_2}
{S : Type u_3}
[inst : Zero M]
[inst : CommSemiring R]
[inst : CommSemiring S]
(h : R →+* S)
(f : α →₀ M)
(g : α → M → R)
:
↑h (Finsupp.prod f g) = Finsupp.prod f fun a b => ↑h (g a b)
Deprecated, use _root_.map_finsupp_prod instead.
theorem
AddMonoidHom.coe_finsupp_sum
{α : Type u_4}
{β : Type u_1}
{N : Type u_2}
{P : Type u_3}
[inst : Zero β]
[inst : AddMonoid N]
[inst : AddCommMonoid P]
(f : α →₀ β)
(g : α → β → N →+ P)
:
↑(Finsupp.sum f g) = Finsupp.sum f fun i fi => ↑(g i fi)
theorem
MonoidHom.coe_finsupp_prod
{α : Type u_4}
{β : Type u_1}
{N : Type u_2}
{P : Type u_3}
[inst : Zero β]
[inst : Monoid N]
[inst : CommMonoid P]
(f : α →₀ β)
(g : α → β → N →* P)
:
↑(Finsupp.prod f g) = Finsupp.prod f fun i fi => ↑(g i fi)
@[simp]
theorem
AddMonoidHom.finsupp_sum_apply
{α : Type u_4}
{β : Type u_1}
{N : Type u_2}
{P : Type u_3}
[inst : Zero β]
[inst : AddMonoid N]
[inst : AddCommMonoid P]
(f : α →₀ β)
(g : α → β → N →+ P)
(x : N)
:
↑(Finsupp.sum f g) x = Finsupp.sum f fun i fi => ↑(g i fi) x
@[simp]
theorem
MonoidHom.finsupp_prod_apply
{α : Type u_4}
{β : Type u_1}
{N : Type u_2}
{P : Type u_3}
[inst : Zero β]
[inst : Monoid N]
[inst : CommMonoid P]
(f : α →₀ β)
(g : α → β → N →* P)
(x : N)
:
↑(Finsupp.prod f g) x = Finsupp.prod f fun i fi => ↑(g i fi) x
theorem
Finsupp.single_multiset_sum
{α : Type u_2}
{M : Type u_1}
[inst : AddCommMonoid M]
(s : Multiset M)
(a : α)
:
Finsupp.single a (Multiset.sum s) = Multiset.sum (Multiset.map (Finsupp.single a) s)
theorem
Finsupp.single_finset_sum
{α : Type u_3}
{ι : Type u_2}
{M : Type u_1}
[inst : AddCommMonoid M]
(s : Finset ι)
(f : ι → M)
(a : α)
:
Finsupp.single a (Finset.sum s fun b => f b) = Finset.sum s fun b => Finsupp.single a (f b)
theorem
Finsupp.single_sum
{α : Type u_4}
{ι : Type u_3}
{M : Type u_1}
{N : Type u_2}
[inst : Zero M]
[inst : AddCommMonoid N]
(s : ι →₀ M)
(f : ι → M → N)
(a : α)
:
Finsupp.single a (Finsupp.sum s f) = Finsupp.sum s fun d c => Finsupp.single a (f d c)
theorem
Finsupp.sum_neg_index
{α : Type u_3}
{M : Type u_2}
{G : Type u_1}
[inst : AddGroup G]
[inst : AddCommMonoid M]
{g : α →₀ G}
{h : α → G → M}
(h0 : ∀ (a : α), h a 0 = 0)
:
Finsupp.sum (-g) h = Finsupp.sum g fun a b => h a (-b)
theorem
Finsupp.prod_neg_index
{α : Type u_3}
{M : Type u_2}
{G : Type u_1}
[inst : AddGroup G]
[inst : CommMonoid M]
{g : α →₀ G}
{h : α → G → M}
(h0 : ∀ (a : α), h a 0 = 1)
:
Finsupp.prod (-g) h = Finsupp.prod g fun a b => h a (-b)
theorem
Finsupp.finset_sum_apply
{α : Type u_3}
{ι : Type u_2}
{N : Type u_1}
[inst : AddCommMonoid N]
(S : Finset ι)
(f : ι → α →₀ N)
(a : α)
:
↑(Finset.sum S fun i => f i) a = Finset.sum S fun i => ↑(f i) a
@[simp]
theorem
Finsupp.sum_apply
{α : Type u_3}
{β : Type u_4}
{M : Type u_1}
{N : Type u_2}
[inst : Zero M]
[inst : AddCommMonoid N]
{f : α →₀ M}
{g : α → M → β →₀ N}
{a₂ : β}
:
↑(Finsupp.sum f g) a₂ = Finsupp.sum f fun a₁ b => ↑(g a₁ b) a₂
theorem
Finsupp.coe_finset_sum
{α : Type u_3}
{ι : Type u_2}
{N : Type u_1}
[inst : AddCommMonoid N]
(S : Finset ι)
(f : ι → α →₀ N)
:
↑(Finset.sum S fun i => f i) = Finset.sum S fun i => ↑(f i)
theorem
Finsupp.coe_sum
{α : Type u_3}
{β : Type u_4}
{M : Type u_1}
{N : Type u_2}
[inst : Zero M]
[inst : AddCommMonoid N]
(f : α →₀ M)
(g : α → M → β →₀ N)
:
↑(Finsupp.sum f g) = Finsupp.sum f fun a₁ b => ↑(g a₁ b)
theorem
Finsupp.support_sum
{α : Type u_4}
{β : Type u_1}
{M : Type u_2}
{N : Type u_3}
[inst : DecidableEq β]
[inst : Zero M]
[inst : AddCommMonoid N]
{f : α →₀ M}
{g : α → M → β →₀ N}
:
(Finsupp.sum f g).support ⊆ Finset.bunionᵢ f.support fun a => (g a (↑f a)).support
theorem
Finsupp.support_finset_sum
{α : Type u_3}
{β : Type u_1}
{M : Type u_2}
[inst : DecidableEq β]
[inst : AddCommMonoid M]
{s : Finset α}
{f : α → β →₀ M}
:
(Finset.sum s f).support ⊆ Finset.bunionᵢ s fun x => (f x).support
@[simp]
theorem
Finsupp.sum_zero
{α : Type u_3}
{M : Type u_1}
{N : Type u_2}
[inst : Zero M]
[inst : AddCommMonoid N]
{f : α →₀ M}
:
(Finsupp.sum f fun x x => 0) = 0
@[simp]
theorem
Finsupp.sum_add
{α : Type u_3}
{M : Type u_1}
{N : Type u_2}
[inst : Zero M]
[inst : AddCommMonoid N]
{f : α →₀ M}
{h₁ : α → M → N}
{h₂ : α → M → N}
:
(Finsupp.sum f fun a b => h₁ a b + h₂ a b) = Finsupp.sum f h₁ + Finsupp.sum f h₂
@[simp]
theorem
Finsupp.prod_mul
{α : Type u_3}
{M : Type u_1}
{N : Type u_2}
[inst : Zero M]
[inst : CommMonoid N]
{f : α →₀ M}
{h₁ : α → M → N}
{h₂ : α → M → N}
:
(Finsupp.prod f fun a b => h₁ a b * h₂ a b) = Finsupp.prod f h₁ * Finsupp.prod f h₂
@[simp]
theorem
Finsupp.sum_neg
{α : Type u_3}
{M : Type u_1}
{G : Type u_2}
[inst : Zero M]
[inst : AddCommGroup G]
{f : α →₀ M}
{h : α → M → G}
:
(Finsupp.sum f fun a b => -h a b) = -Finsupp.sum f h
@[simp]
theorem
Finsupp.prod_inv
{α : Type u_3}
{M : Type u_1}
{G : Type u_2}
[inst : Zero M]
[inst : CommGroup G]
{f : α →₀ M}
{h : α → M → G}
:
(Finsupp.prod f fun a b => (h a b)⁻¹) = (Finsupp.prod f h)⁻¹
@[simp]
theorem
Finsupp.sum_sub
{α : Type u_3}
{M : Type u_1}
{G : Type u_2}
[inst : Zero M]
[inst : AddCommGroup G]
{f : α →₀ M}
{h₁ : α → M → G}
{h₂ : α → M → G}
:
(Finsupp.sum f fun a b => h₁ a b - h₂ a b) = Finsupp.sum f h₁ - Finsupp.sum f h₂
theorem
Finsupp.sum_add_index
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
[inst : DecidableEq α]
[inst : AddZeroClass M]
[inst : AddCommMonoid N]
{f : α →₀ M}
{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₂)
:
Finsupp.sum (f + g) h = Finsupp.sum f h + Finsupp.sum g 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_2}
{N : Type u_3}
[inst : DecidableEq α]
[inst : AddZeroClass M]
[inst : CommMonoid N]
{f : α →₀ M}
{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₂)
:
Finsupp.prod (f + g) h = Finsupp.prod f h * Finsupp.prod g 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_3}
{M : Type u_1}
{N : Type u_2}
[inst : AddZeroClass M]
[inst : AddCommMonoid N]
{f : α →₀ M}
{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₂)
:
Finsupp.sum (f + g) h = Finsupp.sum f h + Finsupp.sum g 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_3}
{M : Type u_1}
{N : Type u_2}
[inst : AddZeroClass M]
[inst : CommMonoid N]
{f : α →₀ M}
{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₂)
:
Finsupp.prod (f + g) h = Finsupp.prod f h * Finsupp.prod g 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_3}
{M : Type u_1}
{N : Type u_2}
[inst : AddZeroClass M]
[inst : AddCommMonoid N]
{f : α →₀ M}
{g : α →₀ M}
(h : α → M →+ N)
:
(Finsupp.sum (f + g) fun x => ↑(h x)) = (Finsupp.sum f fun x => ↑(h x)) + Finsupp.sum g fun x => ↑(h x)
@[simp]
theorem
Finsupp.prod_hom_add_index
{α : Type u_3}
{M : Type u_1}
{N : Type u_2}
[inst : AddZeroClass M]
[inst : CommMonoid N]
{f : α →₀ M}
{g : α →₀ M}
(h : α → Multiplicative M →* N)
:
(Finsupp.prod (f + g) fun a b => ↑(h a) (↑Multiplicative.ofAdd b)) = (Finsupp.prod f fun a b => ↑(h a) (↑Multiplicative.ofAdd b)) * Finsupp.prod g fun a b => ↑(h a) (↑Multiplicative.ofAdd b)
def
Finsupp.liftAddHom
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
[inst : AddZeroClass M]
[inst : AddCommMonoid 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.
@[simp]
theorem
Finsupp.liftAddHom_apply
{α : Type u_3}
{M : Type u_1}
{N : Type u_2}
[inst : AddCommMonoid M]
[inst : AddCommMonoid N]
(F : α → M →+ N)
(f : α →₀ M)
:
↑(↑Finsupp.liftAddHom F) f = Finsupp.sum f fun x => ↑(F x)
@[simp]
theorem
Finsupp.liftAddHom_symm_apply
{α : Type u_3}
{M : Type u_1}
{N : Type u_2}
[inst : AddCommMonoid M]
[inst : AddCommMonoid N]
(F : (α →₀ M) →+ N)
(x : α)
:
↑(AddEquiv.symm Finsupp.liftAddHom) F x = AddMonoidHom.comp F (Finsupp.singleAddHom x)
theorem
Finsupp.liftAddHom_symm_apply_apply
{α : Type u_3}
{M : Type u_1}
{N : Type u_2}
[inst : AddCommMonoid M]
[inst : AddCommMonoid N]
(F : (α →₀ M) →+ N)
(x : α)
(y : M)
:
↑(↑(AddEquiv.symm Finsupp.liftAddHom) F x) y = ↑F (Finsupp.single x y)
@[simp]
theorem
Finsupp.liftAddHom_singleAddHom
{α : Type u_2}
{M : Type u_1}
[inst : AddCommMonoid M]
:
↑Finsupp.liftAddHom Finsupp.singleAddHom = AddMonoidHom.id (α →₀ M)
@[simp]
theorem
Finsupp.sum_single
{α : Type u_2}
{M : Type u_1}
[inst : AddCommMonoid M]
(f : α →₀ M)
:
Finsupp.sum f Finsupp.single = f
@[simp]
theorem
Finsupp.sum_univ_single
{α : Type u_2}
{M : Type u_1}
[inst : AddCommMonoid M]
[inst : Fintype α]
(i : α)
(m : M)
:
(Finset.sum Finset.univ fun j => ↑(Finsupp.single i m) j) = m
@[simp]
theorem
Finsupp.sum_univ_single'
{α : Type u_2}
{M : Type u_1}
[inst : AddCommMonoid M]
[inst : Fintype α]
(i : α)
(m : M)
:
(Finset.sum Finset.univ fun j => ↑(Finsupp.single j m) i) = m
theorem
Finsupp.liftAddHom_apply_single
{α : Type u_3}
{M : Type u_1}
{N : Type u_2}
[inst : AddCommMonoid M]
[inst : AddCommMonoid N]
(f : α → M →+ N)
(a : α)
(b : M)
:
↑(↑Finsupp.liftAddHom f) (Finsupp.single a b) = ↑(f a) b
@[simp]
theorem
Finsupp.liftAddHom_comp_single
{α : Type u_3}
{M : Type u_1}
{N : Type u_2}
[inst : AddCommMonoid M]
[inst : AddCommMonoid N]
(f : α → M →+ N)
(a : α)
:
AddMonoidHom.comp (↑Finsupp.liftAddHom f) (Finsupp.singleAddHom a) = f a
theorem
Finsupp.comp_liftAddHom
{α : Type u_4}
{M : Type u_1}
{N : Type u_2}
{P : Type u_3}
[inst : AddCommMonoid M]
[inst : AddCommMonoid N]
[inst : AddCommMonoid P]
(g : N →+ P)
(f : α → M →+ N)
:
AddMonoidHom.comp g (↑Finsupp.liftAddHom f) = ↑Finsupp.liftAddHom fun a => AddMonoidHom.comp g (f a)
theorem
Finsupp.sum_sub_index
{α : Type u_3}
{γ : Type u_2}
{β : Type u_1}
[inst : AddCommGroup β]
[inst : AddCommGroup γ]
{f : α →₀ β}
{g : α →₀ β}
{h : α → β → γ}
(h_sub : ∀ (a : α) (b₁ b₂ : β), h a (b₁ - b₂) = h a b₁ - h a b₂)
:
Finsupp.sum (f - g) h = Finsupp.sum f h - Finsupp.sum g h
theorem
Finsupp.sum_embDomain
{α : Type u_3}
{β : Type u_4}
{M : Type u_1}
{N : Type u_2}
[inst : Zero M]
[inst : AddCommMonoid N]
{v : α →₀ M}
{f : α ↪ β}
{g : β → M → N}
:
Finsupp.sum (Finsupp.embDomain f v) g = Finsupp.sum v fun a b => g (↑f a) b
theorem
Finsupp.prod_embDomain
{α : Type u_3}
{β : Type u_4}
{M : Type u_1}
{N : Type u_2}
[inst : Zero M]
[inst : CommMonoid N]
{v : α →₀ M}
{f : α ↪ β}
{g : β → M → N}
:
Finsupp.prod (Finsupp.embDomain f v) g = Finsupp.prod v fun a b => g (↑f a) b
theorem
Finsupp.sum_finset_sum_index
{α : Type u_4}
{ι : Type u_3}
{M : Type u_1}
{N : Type u_2}
[inst : AddCommMonoid M]
[inst : AddCommMonoid 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₂)
:
(Finset.sum s fun i => Finsupp.sum (g i) h) = Finsupp.sum (Finset.sum s fun i => g i) h
theorem
Finsupp.prod_finset_sum_index
{α : Type u_4}
{ι : Type u_3}
{M : Type u_1}
{N : Type u_2}
[inst : AddCommMonoid M]
[inst : CommMonoid 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₂)
:
(Finset.prod s fun i => Finsupp.prod (g i) h) = Finsupp.prod (Finset.sum s fun i => g i) h
theorem
Finsupp.sum_sum_index
{α : Type u_4}
{β : Type u_5}
{M : Type u_1}
{N : Type u_2}
{P : Type u_3}
[inst : AddCommMonoid M]
[inst : AddCommMonoid N]
[inst : AddCommMonoid 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₂)
:
Finsupp.sum (Finsupp.sum f g) h = Finsupp.sum f fun a b => Finsupp.sum (g a b) h
theorem
Finsupp.prod_sum_index
{α : Type u_4}
{β : Type u_5}
{M : Type u_1}
{N : Type u_2}
{P : Type u_3}
[inst : AddCommMonoid M]
[inst : AddCommMonoid N]
[inst : CommMonoid 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₂)
:
Finsupp.prod (Finsupp.sum f g) h = Finsupp.prod f fun a b => Finsupp.prod (g a b) h
theorem
Finsupp.multiset_sum_sum_index
{α : Type u_3}
{M : Type u_1}
{N : Type u_2}
[inst : AddCommMonoid M]
[inst : AddCommMonoid 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₂)
:
Finsupp.sum (Multiset.sum f) h = Multiset.sum (Multiset.map (fun g => Finsupp.sum g h) f)
theorem
Finsupp.support_sum_eq_bunionᵢ
{α : Type u_1}
{ι : Type u_2}
{M : Type u_3}
[inst : DecidableEq α]
[inst : AddCommMonoid M]
{g : ι → α →₀ M}
(s : Finset ι)
(h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support)
:
(Finset.sum s fun i => g i).support = Finset.bunionᵢ s fun i => (g i).support
theorem
Finsupp.multiset_map_sum
{α : Type u_2}
{γ : Type u_4}
{β : Type u_3}
{M : Type u_1}
[inst : Zero M]
{f : α →₀ M}
{m : β → γ}
{h : α → M → Multiset β}
:
Multiset.map m (Finsupp.sum f h) = Finsupp.sum f fun a b => Multiset.map m (h a b)
theorem
Finsupp.multiset_sum_sum
{α : Type u_3}
{M : Type u_1}
{N : Type u_2}
[inst : Zero M]
[inst : AddCommMonoid N]
{f : α →₀ M}
{h : α → M → Multiset N}
:
Multiset.sum (Finsupp.sum f h) = Finsupp.sum f fun a b => Multiset.sum (h a b)
theorem
Finsupp.sum_add_index_of_disjoint
{α : Type u_2}
{M : Type u_1}
[inst : AddCommMonoid M]
{f1 : α →₀ M}
{f2 : α →₀ M}
(hd : Disjoint f1.support f2.support)
{β : Type u_3}
[inst : AddCommMonoid β]
(g : α → M → β)
:
Finsupp.sum (f1 + f2) g = Finsupp.sum f1 g + Finsupp.sum f2 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_2}
{M : Type u_1}
[inst : AddCommMonoid M]
{f1 : α →₀ M}
{f2 : α →₀ M}
(hd : Disjoint f1.support f2.support)
{β : Type u_3}
[inst : CommMonoid β]
(g : α → M → β)
:
Finsupp.prod (f1 + f2) g = Finsupp.prod f1 g * Finsupp.prod f2 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_3}
{M : Type u_1}
{N : Type u_2}
[inst : AddCommMonoid M]
[inst : CommMonoid N]
{f1 : α →₀ M}
{f2 : α →₀ M}
{g1 : α → M → N}
{g2 : α → M → N}
(h1 : f1.support ⊆ f2.support)
(h2 : ∀ (a : α), a ∈ f1.support → g1 a (↑f1 a) ∣ g2 a (↑f2 a))
:
Finsupp.prod f1 g1 ∣ Finsupp.prod f2 g2
theorem
Finsupp.indicator_eq_sum_single
{α : Type u_2}
{M : Type u_1}
[inst : AddCommMonoid M]
(s : Finset α)
(f : (a : α) → a ∈ s → M)
:
Finsupp.indicator s f = Finset.sum (Finset.attach s) fun x => Finsupp.single (↑x) (f ↑x (_ : ↑x ∈ s))
@[simp]
theorem
Finsupp.sum_indicator_index
{α : Type u_3}
{M : Type u_1}
{N : Type u_2}
[inst : Zero M]
[inst : AddCommMonoid N]
{s : Finset α}
(f : (a : α) → a ∈ s → M)
{h : α → M → N}
(h_zero : ∀ (a : α), a ∈ s → h a 0 = 0)
:
Finsupp.sum (Finsupp.indicator s f) h = Finset.sum (Finset.attach s) fun x => h (↑x) (f ↑x (_ : ↑x ∈ s))
@[simp]
theorem
Finsupp.prod_indicator_index
{α : Type u_3}
{M : Type u_1}
{N : Type u_2}
[inst : Zero M]
[inst : CommMonoid N]
{s : Finset α}
(f : (a : α) → a ∈ s → M)
{h : α → M → N}
(h_zero : ∀ (a : α), a ∈ s → h a 0 = 1)
:
Finsupp.prod (Finsupp.indicator s f) h = Finset.prod (Finset.attach s) fun x => h (↑x) (f ↑x (_ : ↑x ∈ s))
theorem
Finset.sum_apply'
{α : Type u_3}
{ι : Type u_2}
{A : Type u_1}
[inst : AddCommMonoid A]
{s : Finset α}
{f : α → ι →₀ A}
(i : ι)
:
↑(Finset.sum s fun k => f k) i = Finset.sum s fun k => ↑(f k) i
theorem
Finsupp.sum_apply'
{ι : Type u_2}
{γ : Type u_4}
{A : Type u_3}
{B : Type u_1}
[inst : AddCommMonoid A]
[inst : AddCommMonoid B]
(g : ι →₀ A)
(k : ι → A → γ → B)
(x : γ)
:
Finsupp.sum ι A (γ → B) AddMonoid.toZero Pi.addCommMonoid g k x = Finsupp.sum g fun i b => k i b x
theorem
Finsupp.sum_sum_index'
{α : Type u_4}
{ι : Type u_2}
{A : Type u_3}
{C : Type u_1}
[inst : AddCommMonoid A]
[inst : AddCommMonoid 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}
:
Finsupp.sum (Finset.sum s fun x => f x) t = Finset.sum s fun x => Finsupp.sum (f x) t
theorem
Finsupp.sum_mul
{α : Type u_1}
{R : Type u_2}
{S : Type u_3}
[inst : NonUnitalNonAssocSemiring R]
[inst : NonUnitalNonAssocSemiring S]
(b : S)
(s : α →₀ R)
{f : α → R → S}
:
Finsupp.sum s f * b = Finsupp.sum s fun a c => f a c * b
theorem
Finsupp.mul_sum
{α : Type u_1}
{R : Type u_2}
{S : Type u_3}
[inst : NonUnitalNonAssocSemiring R]
[inst : NonUnitalNonAssocSemiring S]
(b : S)
(s : α →₀ R)
{f : α → R → S}
:
b * Finsupp.sum s f = Finsupp.sum s fun a c => b * f a c