mathlib documentation

data.finsupp.basic

Type of functions with finite support #

For any type α and a type M with zero, we define the type finsupp α M (notation: α →₀ M) of finitely supported functions from α to M, i.e. the functions which are zero everywhere on α except on a finite set.

Functions with finite support are used (at least) in the following parts of the library:

Some other constructions are naturally equivalent to α →₀ M with some α and M but are defined in a different way in the library:

Most of the theory assumes that the range is a commutative additive monoid. This gives us the big sum operator as a powerful way to construct finsupp elements.

Many constructions based on α →₀ M use semireducible type tags to avoid reusing unwanted type instances. E.g., monoid_algebra, add_monoid_algebra, and types based on these two have non-pointwise multiplication.

Notations #

This file adds α →₀ M as a global notation for finsupp α M. We also use the following convention for Type* variables in this file

TODO #

Implementation notes #

This file is a noncomputable theory and uses classical logic throughout.

Notation #

This file defines α →₀ β as notation for finsupp α β.

structure finsupp (α : Type u_13) (M : Type u_14) [has_zero M] :
Type (max u_13 u_14)

finsupp α M, denoted α →₀ M, is the type of functions f : α → M such that f x = 0 for all but finitely many x.

Basic declarations about finsupp #

@[protected, instance]
def finsupp.has_coe_to_fun {α : Type u_1} {M : Type u_5} [has_zero M] :
has_coe_to_fun →₀ M) (λ (_x : α →₀ M), α → M)
Equations
@[simp]
theorem finsupp.coe_mk {α : Type u_1} {M : Type u_5} [has_zero M] (f : α → M) (s : finset α) (h : ∀ (a : α), a s f a 0) :
@[protected, instance]
def finsupp.has_zero {α : Type u_1} {M : Type u_5} [has_zero M] :
Equations
@[simp]
theorem finsupp.coe_zero {α : Type u_1} {M : Type u_5} [has_zero M] :
0 = 0
theorem finsupp.zero_apply {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} :
0 a = 0
@[simp]
theorem finsupp.support_zero {α : Type u_1} {M : Type u_5} [has_zero M] :
@[protected, instance]
def finsupp.inhabited {α : Type u_1} {M : Type u_5} [has_zero M] :
Equations
@[simp]
theorem finsupp.mem_support_iff {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} {a : α} :
a f.support f a 0
@[simp, norm_cast]
theorem finsupp.fun_support_eq {α : Type u_1} {M : Type u_5} [has_zero M] (f : α →₀ M) :
theorem finsupp.not_mem_support_iff {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} {a : α} :
a f.support f a = 0
theorem finsupp.coe_fn_injective {α : Type u_1} {M : Type u_5} [has_zero M] :
@[simp, norm_cast]
theorem finsupp.coe_fn_inj {α : Type u_1} {M : Type u_5} [has_zero M] {f g : α →₀ M} :
f = g f = g
@[simp, norm_cast]
theorem finsupp.coe_eq_zero {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} :
f = 0 f = 0
@[ext]
theorem finsupp.ext {α : Type u_1} {M : Type u_5} [has_zero M] {f g : α →₀ M} (h : ∀ (a : α), f a = g a) :
f = g
theorem finsupp.ext_iff {α : Type u_1} {M : Type u_5} [has_zero M] {f g : α →₀ M} :
f = g ∀ (a : α), f a = g a
theorem finsupp.ext_iff' {α : Type u_1} {M : Type u_5} [has_zero M] {f g : α →₀ M} :
f = g f.support = g.support ∀ (x : α), x f.supportf x = g x
theorem finsupp.congr_fun {α : Type u_1} {M : Type u_5} [has_zero M] {f g : α →₀ M} (h : f = g) (a : α) :
f a = g a
@[simp]
theorem finsupp.support_eq_empty {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} :
f.support = f = 0
theorem finsupp.support_nonempty_iff {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} :
theorem finsupp.nonzero_iff_exists {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} :
f 0 ∃ (a : α), f a 0
theorem finsupp.card_support_eq_zero {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} :
f.support.card = 0 f = 0
@[protected, instance]
def finsupp.decidable_eq {α : Type u_1} {M : Type u_5} [has_zero M] [decidable_eq α] [decidable_eq M] :
Equations
theorem finsupp.finite_support {α : Type u_1} {M : Type u_5} [has_zero M] (f : α →₀ M) :
theorem finsupp.support_subset_iff {α : Type u_1} {M : Type u_5} [has_zero M] {s : set α} {f : α →₀ M} :
(f.support) s ∀ (a : α), a sf a = 0
@[simp]
theorem finsupp.equiv_fun_on_fintype_symm_apply_to_fun {α : Type u_1} {M : Type u_5} [has_zero M] [fintype α] (f : α → M) (ᾰ : α) :
@[simp]
theorem finsupp.equiv_fun_on_fintype_apply {α : Type u_1} {M : Type u_5} [has_zero M] [fintype α] (f : α →₀ M) (a : α) :
@[simp]
theorem finsupp.equiv_fun_on_fintype_symm_apply_support {α : Type u_1} {M : Type u_5} [has_zero M] [fintype α] (f : α → M) :
noncomputable def finsupp.equiv_fun_on_fintype {α : Type u_1} {M : Type u_5} [has_zero M] [fintype α] :
→₀ M) (α → M)

Given fintype α, equiv_fun_on_fintype is the equiv between α →₀ β and α → β. (All functions on a finite type are finitely supported.)

Equations
@[simp]
theorem finsupp.equiv_fun_on_fintype_symm_coe {M : Type u_5} [has_zero M] {α : Type u_1} [fintype α] (f : α →₀ M) :

Declarations about single #

noncomputable def finsupp.single {α : Type u_1} {M : Type u_5} [has_zero M] (a : α) (b : M) :
α →₀ M

single a b is the finitely supported function which has value b at a and zero otherwise.

Equations
theorem finsupp.single_apply {α : Type u_1} {M : Type u_5} [has_zero M] {a a' : α} {b : M} [decidable (a = a')] :
(finsupp.single a b) a' = ite (a = a') b 0
theorem finsupp.single_eq_indicator {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} {b : M} :
(finsupp.single a b) = {a}.indicator (λ (_x : α), b)
@[simp]
theorem finsupp.single_eq_same {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} {b : M} :
@[simp]
theorem finsupp.single_eq_of_ne {α : Type u_1} {M : Type u_5} [has_zero M] {a a' : α} {b : M} (h : a a') :
(finsupp.single a b) a' = 0
theorem finsupp.single_eq_update {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} {b : M} [decidable_eq α] :
theorem finsupp.single_eq_pi_single {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} {b : M} [decidable_eq α] :
@[simp]
theorem finsupp.single_zero {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} :
theorem finsupp.single_of_single_apply {α : Type u_1} {M : Type u_5} [has_zero M] (a a' : α) (b : M) :
theorem finsupp.support_single_ne_zero {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} {b : M} (hb : b 0) :
theorem finsupp.support_single_subset {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} {b : M} :
theorem finsupp.single_apply_mem {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} {b : M} (x : α) :
(finsupp.single a b) x {0, b}
theorem finsupp.range_single_subset {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} {b : M} :
theorem finsupp.single_injective {α : Type u_1} {M : Type u_5} [has_zero M] (a : α) :

finsupp.single a b is injective in b. For the statement that it is injective in a, see finsupp.single_left_injective

theorem finsupp.single_apply_eq_zero {α : Type u_1} {M : Type u_5} [has_zero M] {a x : α} {b : M} :
(finsupp.single a b) x = 0 x = ab = 0
theorem finsupp.mem_support_single {α : Type u_1} {M : Type u_5} [has_zero M] (a a' : α) (b : M) :
a (finsupp.single a' b).support a = a' b 0
theorem finsupp.eq_single_iff {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} {a : α} {b : M} :
f = finsupp.single a b f.support {a} f a = b
theorem finsupp.single_eq_single_iff {α : Type u_1} {M : Type u_5} [has_zero M] (a₁ a₂ : α) (b₁ b₂ : M) :
finsupp.single a₁ b₁ = finsupp.single a₂ b₂ a₁ = a₂ b₁ = b₂ b₁ = 0 b₂ = 0
theorem finsupp.single_left_injective {α : Type u_1} {M : Type u_5} [has_zero M] {b : M} (h : b 0) :

finsupp.single a b is injective in a. For the statement that it is injective in b, see finsupp.single_injective

theorem finsupp.single_left_inj {α : Type u_1} {M : Type u_5} [has_zero M] {a a' : α} {b : M} (h : b 0) :
theorem finsupp.support_single_ne_bot {α : Type u_1} {M : Type u_5} [has_zero M] {b : M} (i : α) (h : b 0) :
theorem finsupp.support_single_disjoint {α : Type u_1} {M : Type u_5} [has_zero M] {b : M} [decidable_eq α] {b' : M} (hb : b 0) (hb' : b' 0) {i j : α} :
@[simp]
theorem finsupp.single_eq_zero {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} {b : M} :
finsupp.single a b = 0 b = 0
theorem finsupp.single_swap {α : Type u_1} {M : Type u_5} [has_zero M] (a₁ a₂ : α) (b : M) :
(finsupp.single a₁ b) a₂ = (finsupp.single a₂ b) a₁
@[protected, instance]
def finsupp.nontrivial {α : Type u_1} {M : Type u_5} [has_zero M] [nonempty α] [nontrivial M] :
theorem finsupp.unique_single {α : Type u_1} {M : Type u_5} [has_zero M] [unique α] (x : α →₀ M) :
theorem finsupp.unique_ext {α : Type u_1} {M : Type u_5} [has_zero M] [unique α] {f g : α →₀ M} (h : f (default α) = g (default α)) :
f = g
theorem finsupp.unique_ext_iff {α : Type u_1} {M : Type u_5} [has_zero M] [unique α] {f g : α →₀ M} :
f = g f (default α) = g (default α)
@[simp]
theorem finsupp.unique_single_eq_iff {α : Type u_1} {M : Type u_5} [has_zero M] {a a' : α} {b : M} [unique α] {b' : M} :
theorem finsupp.support_eq_singleton {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} {a : α} :
f.support = {a} f a 0 f = finsupp.single a (f a)
theorem finsupp.support_eq_singleton' {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} {a : α} :
f.support = {a} ∃ (b : M) (H : b 0), f = finsupp.single a b
theorem finsupp.card_support_eq_one {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} :
f.support.card = 1 ∃ (a : α), f a 0 f = finsupp.single a (f a)
theorem finsupp.card_support_eq_one' {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} :
f.support.card = 1 ∃ (a : α) (b : M) (H : b 0), f = finsupp.single a b
theorem finsupp.support_subset_singleton {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} {a : α} :
theorem finsupp.support_subset_singleton' {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} {a : α} :
f.support {a} ∃ (b : M), f = finsupp.single a b
theorem finsupp.card_support_le_one {α : Type u_1} {M : Type u_5} [has_zero M] [nonempty α] {f : α →₀ M} :
f.support.card 1 ∃ (a : α), f = finsupp.single a (f a)
theorem finsupp.card_support_le_one' {α : Type u_1} {M : Type u_5} [has_zero M] [nonempty α] {f : α →₀ M} :
f.support.card 1 ∃ (a : α) (b : M), f = finsupp.single a b
@[simp]
theorem finsupp.equiv_fun_on_fintype_single {α : Type u_1} {M : Type u_5} [has_zero M] [decidable_eq α] [fintype α] (x : α) (m : M) :
@[simp]
theorem finsupp.equiv_fun_on_fintype_symm_single {α : Type u_1} {M : Type u_5} [has_zero M] [decidable_eq α] [fintype α] (x : α) (m : M) :

Declarations about update #

noncomputable def finsupp.update {α : Type u_1} {M : Type u_5} [has_zero M] (f : α →₀ M) (a : α) (b : M) :
α →₀ M

Replace the value of a α →₀ M at a given point a : α by a given value b : M. If b = 0, this amounts to removing a from the finsupp.support. Otherwise, if a was not in the finsupp.support, it is added to it.

This is the finitely-supported version of function.update.

Equations
@[simp]
theorem finsupp.coe_update {α : Type u_1} {M : Type u_5} [has_zero M] (f : α →₀ M) (a : α) (b : M) [decidable_eq α] :
@[simp]
theorem finsupp.update_self {α : Type u_1} {M : Type u_5} [has_zero M] (f : α →₀ M) (a : α) :
f.update a (f a) = f
theorem finsupp.support_update {α : Type u_1} {M : Type u_5} [has_zero M] (f : α →₀ M) (a : α) (b : M) [decidable_eq α] :
(f.update a b).support = ite (b = 0) (f.support.erase a) (insert a f.support)
@[simp]
theorem finsupp.support_update_zero {α : Type u_1} {M : Type u_5} [has_zero M] (f : α →₀ M) (a : α) [decidable_eq α] :
theorem finsupp.support_update_ne_zero {α : Type u_1} {M : Type u_5} [has_zero M] (f : α →₀ M) (a : α) {b : M} [decidable_eq α] (h : b 0) :

Declarations about on_finset #

noncomputable def finsupp.on_finset {α : Type u_1} {M : Type u_5} [has_zero M] (s : finset α) (f : α → M) (hf : ∀ (a : α), f a 0a s) :
α →₀ M

on_finset s f hf is the finsupp function representing f restricted to the finset s. The function needs to be 0 outside of s. Use this when the set needs to be filtered anyways, otherwise a better set representation is often available.

Equations
@[simp]
theorem finsupp.on_finset_apply {α : Type u_1} {M : Type u_5} [has_zero M] {s : finset α} {f : α → M} {hf : ∀ (a : α), f a 0a s} {a : α} :
(finsupp.on_finset s f hf) a = f a
@[simp]
theorem finsupp.support_on_finset_subset {α : Type u_1} {M : Type u_5} [has_zero M] {s : finset α} {f : α → M} {hf : ∀ (a : α), f a 0a s} :
@[simp]
theorem finsupp.mem_support_on_finset {α : Type u_1} {M : Type u_5} [has_zero M] {s : finset α} {f : α → M} (hf : ∀ (a : α), f a 0a s) {a : α} :
theorem finsupp.support_on_finset {α : Type u_1} {M : Type u_5} [has_zero M] {s : finset α} {f : α → M} (hf : ∀ (a : α), f a 0a s) :
(finsupp.on_finset s f hf).support = finset.filter (λ (a : α), f a 0) s
noncomputable def finsupp.of_support_finite {α : Type u_1} {M : Type u_5} [has_zero M] (f : α → M) (hf : (function.support f).finite) :
α →₀ M

The natural finsupp induced by the function f given that it has finite support.

Equations
theorem finsupp.of_support_finite_coe {α : Type u_1} {M : Type u_5} [has_zero M] {f : α → M} {hf : (function.support f).finite} :
@[protected, instance]
def finsupp.can_lift {α : Type u_1} {M : Type u_5} [has_zero M] :
can_lift (α → M) →₀ M)
Equations

Declarations about map_range #

noncomputable def finsupp.map_range {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [has_zero N] (f : M → N) (hf : f 0 = 0) (g : α →₀ M) :
α →₀ N

The composition of f : M → N and g : α →₀ M is map_range f hf g : α →₀ N, well-defined when f 0 = 0.

This preserves the structure on f, and exists in various bundled forms for when f is itself bundled:

Equations
@[simp]
theorem finsupp.map_range_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [has_zero N] {f : M → N} {hf : f 0 = 0} {g : α →₀ M} {a : α} :
(finsupp.map_range f hf g) a = f (g a)
@[simp]
theorem finsupp.map_range_zero {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [has_zero N] {f : M → N} {hf : f 0 = 0} :
@[simp]
theorem finsupp.map_range_id {α : Type u_1} {M : Type u_5} [has_zero M] (g : α →₀ M) :
theorem finsupp.map_range_comp {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [has_zero M] [has_zero N] [has_zero P] (f : N → P) (hf : f 0 = 0) (f₂ : M → N) (hf₂ : f₂ 0 = 0) (h : (f f₂) 0 = 0) (g : α →₀ M) :
finsupp.map_range (f f₂) h g = finsupp.map_range f hf (finsupp.map_range f₂ hf₂ g)
theorem finsupp.support_map_range {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [has_zero N] {f : M → N} {hf : f 0 = 0} {g : α →₀ M} :
@[simp]
theorem finsupp.map_range_single {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [has_zero N] {f : M → N} {hf : f 0 = 0} {a : α} {b : M} :

Declarations about emb_domain #

noncomputable def finsupp.emb_domain {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (v : α →₀ M) :
β →₀ M

Given f : α ↪ β and v : α →₀ M, emb_domain f v : β →₀ M is the finitely supported function whose value at f a : β is v a. For a b : β outside the range of f, it is zero.

Equations
@[simp]
theorem finsupp.support_emb_domain {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (v : α →₀ M) :
@[simp]
theorem finsupp.emb_domain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) :
@[simp]
theorem finsupp.emb_domain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (v : α →₀ M) (a : α) :
theorem finsupp.emb_domain_notin_range {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (v : α →₀ M) (a : β) (h : a set.range f) :
theorem finsupp.emb_domain_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) :
@[simp]
theorem finsupp.emb_domain_inj {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] {f : α β} {l₁ l₂ : α →₀ M} :
finsupp.emb_domain f l₁ = finsupp.emb_domain f l₂ l₁ = l₂
@[simp]
theorem finsupp.emb_domain_eq_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] {f : α β} {l : α →₀ M} :
theorem finsupp.emb_domain_map_range {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [has_zero M] [has_zero N] (f : α β) (g : M → N) (p : α →₀ M) (hg : g 0 = 0) :
theorem finsupp.single_of_emb_domain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (l : α →₀ M) (f : α β) (a : β) (b : M) (hb : b 0) (h : finsupp.emb_domain f l = finsupp.single a b) :
∃ (x : α), l = finsupp.single x b f x = a
@[simp]
theorem finsupp.emb_domain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (a : α) (m : M) :

Declarations about zip_with #

noncomputable def finsupp.zip_with {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [has_zero M] [has_zero N] [has_zero P] (f : M → N → P) (hf : f 0 0 = 0) (g₁ : α →₀ M) (g₂ : α →₀ N) :
α →₀ P

zip_with f hf g₁ g₂ is the finitely supported function satisfying zip_with f hf g₁ g₂ a = f (g₁ a) (g₂ a), and it is well-defined when f 0 0 = 0.

Equations
@[simp]
theorem finsupp.zip_with_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [has_zero M] [has_zero N] [has_zero P] {f : M → N → P} {hf : f 0 0 = 0} {g₁ : α →₀ M} {g₂ : α →₀ N} {a : α} :
(finsupp.zip_with f hf g₁ g₂) a = f (g₁ a) (g₂ a)
theorem finsupp.support_zip_with {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [has_zero M] [has_zero N] [has_zero P] [D : decidable_eq α] {f : M → N → P} {hf : f 0 0 = 0} {g₁ : α →₀ M} {g₂ : α →₀ N} :
(finsupp.zip_with f hf g₁ g₂).support g₁.support g₂.support

Declarations about erase #

noncomputable def finsupp.erase {α : Type u_1} {M : Type u_5} [has_zero M] (a : α) (f : α →₀ M) :
α →₀ M

erase a f is the finitely supported function equal to f except at a where it is equal to 0.

Equations
@[simp]
theorem finsupp.support_erase {α : Type u_1} {M : Type u_5} [has_zero M] [decidable_eq α] {a : α} {f : α →₀ M} :
@[simp]
theorem finsupp.erase_same {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} {f : α →₀ M} :
@[simp]
theorem finsupp.erase_ne {α : Type u_1} {M : Type u_5} [has_zero M] {a a' : α} {f : α →₀ M} (h : a' a) :
(finsupp.erase a f) a' = f a'
@[simp]
theorem finsupp.erase_single {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} {b : M} :
theorem finsupp.erase_single_ne {α : Type u_1} {M : Type u_5} [has_zero M] {a a' : α} {b : M} (h : a a') :
@[simp]
theorem finsupp.erase_of_not_mem_support {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} {a : α} (haf : a f.support) :
@[simp]
theorem finsupp.erase_zero {α : Type u_1} {M : Type u_5} [has_zero M] (a : α) :

Declarations about sum and prod #

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

def finsupp.prod {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [comm_monoid N] (f : α →₀ M) (g : α → M → N) :
N

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

Equations
def finsupp.sum {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [add_comm_monoid N] (f : α →₀ M) (g : α → M → N) :
N

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

Equations
theorem finsupp.prod_of_support_subset {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [comm_monoid N] (f : α →₀ M) {s : finset α} (hs : f.support s) (g : α → M → N) (h : ∀ (i : α), i sg i 0 = 1) :
f.prod g = ∏ (x : α) in s, g x (f x)
theorem finsupp.sum_of_support_subset {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [add_comm_monoid N] (f : α →₀ M) {s : finset α} (hs : f.support s) (g : α → M → N) (h : ∀ (i : α), i sg i 0 = 0) :
f.sum g = ∑ (x : α) in s, g x (f x)
theorem finsupp.prod_fintype {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [comm_monoid N] [fintype α] (f : α →₀ M) (g : α → M → N) (h : ∀ (i : α), g i 0 = 1) :
f.prod g = ∏ (i : α), g i (f i)
theorem finsupp.sum_fintype {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [add_comm_monoid N] [fintype α] (f : α →₀ M) (g : α → M → N) (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_5} {N : Type u_7} [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_5} {N : Type u_7} [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_5} {M' : Type u_6} {N : Type u_7} [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_5} {M' : Type u_6} {N : Type u_7} [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_5} {N : Type u_7} [has_zero M] [comm_monoid N] {h : α → M → N} :
0.prod h = 1
@[simp]
theorem finsupp.sum_zero_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [add_comm_monoid N] {h : α → M → N} :
0.sum h = 0
theorem finsupp.prod_comm {α : Type u_1} {β : Type u_2} {M : Type u_5} {M' : Type u_6} {N : Type u_7} [has_zero M] [has_zero M'] [comm_monoid N] (f : α →₀ M) (g : β →₀ M') (h : α → M → β → M' → N) :
f.prod (λ (x : α) (v : M), g.prod (λ (x' : β) (v' : M'), h x v x' v')) = g.prod (λ (x' : β) (v' : M'), f.prod (λ (x : α) (v : M), h x v x' v'))
theorem finsupp.sum_comm {α : Type u_1} {β : Type u_2} {M : Type u_5} {M' : Type u_6} {N : Type u_7} [has_zero M] [has_zero M'] [add_comm_monoid N] (f : α →₀ M) (g : β →₀ M') (h : α → M → β → M' → N) :
f.sum (λ (x : α) (v : M), g.sum (λ (x' : β) (v' : M'), h x v x' v')) = g.sum (λ (x' : β) (v' : M'), f.sum (λ (x : α) (v : M), h x v x' v'))
@[simp]
theorem finsupp.prod_ite_eq {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [comm_monoid N] [decidable_eq α] (f : α →₀ M) (a : α) (b : α → M → N) :
f.prod (λ (x : α) (v : M), ite (a = x) (b x v) 1) = ite (a f.support) (b a (f a)) 1
@[simp]
theorem finsupp.sum_ite_eq {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [add_comm_monoid N] [decidable_eq α] (f : α →₀ M) (a : α) (b : α → M → N) :
f.sum (λ (x : α) (v : M), ite (a = x) (b x v) 0) = ite (a f.support) (b a (f a)) 0
@[simp]
theorem finsupp.sum_ite_self_eq {α : Type u_1} [decidable_eq α] {N : Type u_2} [add_comm_monoid N] (f : α →₀ N) (a : α) :
f.sum (λ (x : α) (v : N), ite (a = x) v 0) = f a
@[simp]
theorem finsupp.prod_ite_eq' {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [comm_monoid N] [decidable_eq α] (f : α →₀ M) (a : α) (b : α → M → N) :
f.prod (λ (x : α) (v : M), ite (x = a) (b x v) 1) = ite (a f.support) (b a (f a)) 1

A restatement of prod_ite_eq with the equality test reversed.

@[simp]
theorem finsupp.sum_ite_eq' {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [add_comm_monoid N] [decidable_eq α] (f : α →₀ M) (a : α) (b : α → M → N) :
f.sum (λ (x : α) (v : M), ite (x = a) (b x v) 0) = ite (a f.support) (b a (f a)) 0

A restatement of sum_ite_eq with the equality test reversed.

@[simp]
theorem finsupp.sum_ite_self_eq' {α : Type u_1} [decidable_eq α] {N : Type u_2} [add_comm_monoid N] (f : α →₀ N) (a : α) :
f.sum (λ (x : α) (v : N), ite (x = a) v 0) = f a
@[simp]
theorem finsupp.prod_pow {α : Type u_1} {N : Type u_7} [comm_monoid N] [fintype α] (f : α →₀ ) (g : α → N) :
f.prod (λ (a : α) (b : ), g a ^ b) = ∏ (a : α), g a ^ f a
theorem finsupp.on_finset_prod {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [comm_monoid N] {s : finset α} {f : α → M} {g : α → M → N} (hf : ∀ (a : α), f a 0a s) (hg : ∀ (a : α), g a 0 = 1) :
(finsupp.on_finset s f hf).prod g = ∏ (a : α) in s, 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_5} {N : Type u_7} [has_zero M] [add_comm_monoid N] {s : finset α} {f : α → M} {g : α → M → N} (hf : ∀ (a : α), f a 0a s) (hg : ∀ (a : α), g a 0 = 0) :
(finsupp.on_finset s f hf).sum g = ∑ (a : α) in s, 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_5} {N : Type u_7} [has_zero M] [comm_monoid N] (f : α →₀ M) (y : α) (g : α → M → N) (hyf : y f.support) :
(g y (f y)) * (finsupp.erase y f).prod g = f.prod g

Taking a product over f : α →₀ M is the same as multiplying the value on a single element y ∈ f.support by the product over erase y f.

theorem finsupp.add_sum_erase {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [add_comm_monoid N] (f : α →₀ M) (y : α) (g : α → M → N) (hyf : y f.support) :
g y (f y) + (finsupp.erase y f).sum g = f.sum g

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

theorem finsupp.mul_prod_erase' {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [comm_monoid N] (f : α →₀ M) (y : α) (g : α → M → N) (hg : ∀ (i : α), g i 0 = 1) :
(g y (f y)) * (finsupp.erase y f).prod g = f.prod g

Generalization of finsupp.mul_prod_erase: if g maps a second argument of 0 to 1, then its product over f : α →₀ M is the same as multiplying the value on any element y : α by the product over erase y f.

theorem finsupp.add_sum_erase' {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [add_comm_monoid N] (f : α →₀ M) (y : α) (g : α → M → N) (hg : ∀ (i : α), g i 0 = 0) :
g y (f y) + (finsupp.erase y f).sum g = f.sum g

Generalization of finsupp.add_sum_erase: if g maps a second argument of 0 to 0, then its sum over f : α →₀ M is the same as adding the value on any element y : α to the sum over erase y f.

theorem submonoid.finsupp_prod_mem {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [comm_monoid N] (S : submonoid N) (f : α →₀ M) (g : α → M → N) (h : ∀ (c : α), f c 0g c (f c) S) :
f.prod g S
theorem add_submonoid.finsupp_sum_mem {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [add_comm_monoid N] (S : add_submonoid N) (f : α →₀ M) (g : α → M → N) (h : ∀ (c : α), f c 0g c (f c) S) :
f.sum g S
theorem finsupp.prod_congr {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [comm_monoid N] {f : α →₀ M} {g1 g2 : α → M → N} (h : ∀ (x : α), x f.supportg1 x (f x) = g2 x (f x)) :
f.prod g1 = f.prod g2
theorem finsupp.sum_congr {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [add_comm_monoid N] {f : α →₀ M} {g1 g2 : α → M → N} (h : ∀ (x : α), x f.supportg1 x (f x) = g2 x (f x)) :
f.sum g1 = f.sum g2

Additive monoid structure on α →₀ M #

@[protected, instance]
noncomputable def finsupp.has_add {α : Type u_1} {M : Type u_5} [add_zero_class M] :
Equations
@[simp]
theorem finsupp.coe_add {α : Type u_1} {M : Type u_5} [add_zero_class M] (f g : α →₀ M) :
(f + g) = f + g
theorem finsupp.add_apply {α : Type u_1} {M : Type u_5} [add_zero_class M] (g₁ g₂ : α →₀ M) (a : α) :
(g₁ + g₂) a = g₁ a + g₂ a
theorem finsupp.support_add {α : Type u_1} {M : Type u_5} [add_zero_class M] [decidable_eq α] {g₁ g₂ : α →₀ M} :
(g₁ + g₂).support g₁.support g₂.support
theorem finsupp.support_add_eq {α : Type u_1} {M : Type u_5} [add_zero_class M] [decidable_eq α] {g₁ g₂ : α →₀ M} (h : disjoint g₁.support g₂.support) :
(g₁ + g₂).support = g₁.support g₂.support
@[simp]
theorem finsupp.single_add {α : Type u_1} {M : Type u_5} [add_zero_class M] {a : α} {b₁ b₂ : M} :
finsupp.single a (b₁ + b₂) = finsupp.single a b₁ + finsupp.single a b₂
@[protected, instance]
noncomputable def finsupp.add_zero_class {α : Type u_1} {M : Type u_5} [add_zero_class M] :
Equations
noncomputable def finsupp.single_add_hom {α : Type u_1} {M : Type u_5} [add_zero_class M] (a : α) :
M →+ α →₀ M

finsupp.single as an add_monoid_hom.

See finsupp.lsingle for the stronger version as a linear map.

Equations
@[simp]
theorem finsupp.single_add_hom_apply {α : Type u_1} {M : Type u_5} [add_zero_class M] (a : α) (b : M) :
noncomputable def finsupp.apply_add_hom {α : Type u_1} {M : Type u_5} [add_zero_class M] (a : α) :
→₀ M) →+ M

Evaluation of a function f : α →₀ M at a point as an additive monoid homomorphism.

See finsupp.lapply for the stronger version as a linear map.

Equations
@[simp]
theorem finsupp.apply_add_hom_apply {α : Type u_1} {M : Type u_5} [add_zero_class M] (a : α) (g : α →₀ M) :
theorem finsupp.update_eq_single_add_erase {α : Type u_1} {M : Type u_5} [add_zero_class M] (f : α →₀ M) (a : α) (b : M) :
theorem finsupp.update_eq_erase_add_single {α : Type u_1} {M : Type u_5} [add_zero_class M] (f : α →₀ M) (a : α) (b : M) :
theorem finsupp.single_add_erase {α : Type u_1} {M : Type u_5} [add_zero_class M] (a : α) (f : α →₀ M) :
theorem finsupp.erase_add_single {α : Type u_1} {M : Type u_5} [add_zero_class M] (a : α) (f : α →₀ M) :
@[simp]
theorem finsupp.erase_add {α : Type u_1} {M : Type u_5} [add_zero_class M] (a : α) (f f' : α →₀ M) :
@[simp]
theorem finsupp.erase_add_hom_apply {α : Type u_1} {M : Type u_5} [add_zero_class M] (a : α) (f : α →₀ M) :
noncomputable def finsupp.erase_add_hom {α : Type u_1} {M : Type u_5} [add_zero_class M] (a : α) :
→₀ M) →+ α →₀ M

finsupp.erase as an add_monoid_hom.

Equations
@[protected]
theorem finsupp.induction {α : Type u_1} {M : Type u_5} [add_zero_class M] {p : →₀ M) → Prop} (f : α →₀ M) (h0 : p 0) (ha : ∀ (a : α) (b : M) (f : α →₀ M), a f.supportb 0p fp (finsupp.single a b + f)) :
p f
theorem finsupp.induction₂ {α : Type u_1} {M : Type u_5} [add_zero_class M] {p : →₀ M) → Prop} (f : α →₀ M) (h0 : p 0) (ha : ∀ (a : α) (b : M) (f : α →₀ M), a f.supportb 0p fp (f + finsupp.single a b)) :
p f
theorem finsupp.induction_linear {α : Type u_1} {M : Type u_5} [add_zero_class M] {p : →₀ M) → Prop} (f : α →₀ M) (h0 : p 0) (hadd : ∀ (f g : α →₀ M), p fp gp (f + g)) (hsingle : ∀ (a : α) (b : M), p (finsupp.single a b)) :
p f
@[simp]
theorem finsupp.add_closure_set_of_eq_single {α : Type u_1} {M : Type u_5} [add_zero_class M] :
add_submonoid.closure {f : α →₀ M | ∃ (a : α) (b : M), f = finsupp.single a b} =
theorem finsupp.add_hom_ext {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_zero_class M] [add_zero_class N] ⦃f g : →₀ M) →+ N⦄ (H : ∀ (x : α) (y : M), f (finsupp.single x y) = g (finsupp.single x y)) :
f = g

If two additive homomorphisms from α →₀ M are equal on each single a b, then they are equal.

@[ext]
theorem finsupp.add_hom_ext' {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_zero_class M] [add_zero_class N] ⦃f g : →₀ M) →+ N⦄ (H : ∀ (x : α), f.comp (finsupp.single_add_hom x) = g.comp (finsupp.single_add_hom x)) :
f = g

If two additive homomorphisms from α →₀ M are equal on each single a b, then they are equal.

We formulate this using equality of add_monoid_homs so that ext tactic can apply a type-specific extensionality lemma after this one. E.g., if the fiber M is or , then it suffices to verify f (single a 1) = g (single a 1).

theorem finsupp.mul_hom_ext {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_zero_class M] [mul_one_class N] ⦃f g : multiplicative →₀ M) →* N⦄ (H : ∀ (x : α) (y : M), f (multiplicative.of_add (finsupp.single x y)) = g (multiplicative.of_add (finsupp.single x y))) :
f = g
@[ext]
theorem finsupp.mul_hom_ext' {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_zero_class M] [mul_one_class N] {f g : multiplicative →₀ M) →* N} (H : ∀ (x : α), f.comp (add_monoid_hom.to_multiplicative (finsupp.single_add_hom x)) = g.comp (add_monoid_hom.to_multiplicative (finsupp.single_add_hom x))) :
f = g
theorem finsupp.map_range_add {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_zero_class M] [add_zero_class N] {f : M → N} {hf : f 0 = 0} (hf' : ∀ (x y : M), f (x + y) = f x + f y) (v₁ v₂ : α →₀ M) :
finsupp.map_range f hf (v₁ + v₂) = finsupp.map_range f hf v₁ + finsupp.map_range f hf v₂
@[simp]
theorem finsupp.emb_domain.add_monoid_hom_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_zero_class M] (f : α β) (v : α →₀ M) :
noncomputable def finsupp.emb_domain.add_monoid_hom {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_zero_class M] (f : α β) :
→₀ M) →+ β →₀ M

Bundle emb_domain f as an additive map from α →₀ M to β →₀ M.

Equations
@[simp]
theorem finsupp.emb_domain_add {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_zero_class M] (f : α β) (v w : α →₀ M) :
@[protected, instance]
noncomputable def finsupp.add_monoid {α : Type u_1} {M : Type u_5} [add_monoid M] :
Equations
theorem mul_equiv.map_finsupp_prod {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [has_zero M] [comm_monoid N] [comm_monoid P] (h : N ≃* P) (f : α →₀ M) (g : α → M → N) :
h (f.prod g) = f.prod (λ (a : α) (b : M), h (g a b))
theorem add_equiv.map_finsupp_sum {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [has_zero M] [add_comm_monoid N] [add_comm_monoid P] (h : N ≃+ P) (f : α →₀ M) (g : α → M → N) :
h (f.sum g) = f.sum (λ (a : α) (b : M), h (g a b))
theorem add_monoid_hom.map_finsupp_sum {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [has_zero M] [add_comm_monoid N] [add_comm_monoid P] (h : N →+ P) (f : α →₀ M) (g : α → M → N) :
h (f.sum g) = f.sum (λ (a : α) (b : M), h (g a b))
theorem monoid_hom.map_finsupp_prod {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [has_zero M] [comm_monoid N] [comm_monoid P] (h : N →* P) (f : α →₀ M) (g : α → M → N) :
h (f.prod g) = f.prod (λ (a : α) (b : M), h (g a b))
theorem ring_hom.map_finsupp_sum {α : Type u_1} {M : Type u_5} {R : Type u_11} {S : Type u_12} [has_zero M] [semiring R] [semiring S] (h : R →+* S) (f : α →₀ M) (g : α → M → R) :
h (f.sum g) = f.sum (λ (a : α) (b : M), h (g a b))
theorem ring_hom.map_finsupp_prod {α : Type u_1} {M : Type u_5} {R : Type u_11} {S : Type u_12} [has_zero M] [comm_semiring R] [comm_semiring S] (h : R →+* S) (f : α →₀ M) (g : α → M → R) :
h (f.prod g) = f.prod (λ (a : α) (b : M), h (g a b))
theorem add_monoid_hom.coe_finsupp_sum {α : Type u_1} {β : Type u_2} {N : Type u_7} {P : Type u_8} [has_zero β] [add_monoid N] [add_comm_monoid P] (f : α →₀ β) (g : α → β → N →+ P) :
(f.sum g) = f.sum (λ (i : α) (fi : β), (g i fi))
theorem monoid_hom.coe_finsupp_prod {α : Type u_1} {β : Type u_2} {N : Type u_7} {P : Type u_8} [has_zero β] [monoid N] [comm_monoid P] (f : α →₀ β) (g : α → β → N →* P) :
(f.prod g) = f.prod (λ (i : α) (fi : β), (g i fi))
@[simp]
theorem monoid_hom.finsupp_prod_apply {α : Type u_1} {β : Type u_2} {N : Type u_7} {P : Type u_8} [has_zero β] [monoid N] [comm_monoid P] (f : α →₀ β) (g : α → β → N →* P) (x : N) :
(f.prod g) x = f.prod (λ (i : α) (fi : β), (g i fi) x)
@[simp]
theorem add_monoid_hom.finsupp_sum_apply {α : Type u_1} {β : Type u_2} {N : Type u_7} {P : Type u_8} [has_zero β] [add_monoid N] [add_comm_monoid P] (f : α →₀ β) (g : α → β → N →+ P) (x : N) :
(f.sum g) x = f.sum (λ (i : α) (fi : β), (g i fi) x)
@[protected, instance]
noncomputable def finsupp.has_sub {α : Type u_1} {G : Type u_9} [add_group G] :
Equations
theorem finsupp.single_multiset_sum {α : Type u_1} {M : Type u_5} [add_comm_monoid M] (s : multiset M) (a : α) :
theorem finsupp.single_finset_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} [add_comm_monoid M] (s : finset ι) (f : ι → M) (a : α) :
finsupp.single a (∑ (b : ι) in s, f b) = ∑ (b : ι) in s, finsupp.single a (f b)
theorem finsupp.single_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} {N : Type u_7} [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.prod_neg_index {α : Type u_1} {M : Type u_5} {G : Type u_9} [add_group G] [comm_monoid M] {g : α →₀ G} {h : α → G → M} (h0 : ∀ (a : α), h a 0 = 1) :
(-g).prod h = g.prod (λ (a : α) (b : G), h a (-b))
theorem finsupp.sum_neg_index {α : Type u_1} {M : Type u_5} {G : Type u_9} [add_group G] [add_comm_monoid M] {g : α →₀ G} {h : α → G → M} (h0 : ∀ (a : α), h a 0 = 0) :
(-g).sum h = g.sum (λ (a : α) (b : G), h a (-b))
@[simp]
theorem finsupp.coe_neg {α : Type u_1} {G : Type u_9} [add_group G] (g : α →₀ G) :
theorem finsupp.neg_apply {α : Type u_1} {G : Type u_9} [add_group G] (g : α →₀ G) (a : α) :
(-g) a = -g a
@[simp]
theorem finsupp.coe_sub {α : Type u_1} {G : Type u_9} [add_group G] (g₁ g₂ : α →₀ G) :
(g₁ - g₂) = g₁ - g₂
theorem finsupp.sub_apply {α : Type u_1} {G : Type u_9} [add_group G] (g₁ g₂ : α →₀ G) (a : α) :
(g₁ - g₂) a = g₁ a - g₂ a
@[simp]
theorem finsupp.support_neg {α : Type u_1} {G : Type u_9} [add_group G] (f : α →₀ G) :
theorem finsupp.support_sub {α : Type u_1} {G : Type u_9} [decidable_eq α] [add_group G] {f g : α →₀ G} :
theorem finsupp.erase_eq_sub_single {α : Type u_1} {G : Type u_9} [add_group G] (f : α →₀ G) (a : α) :
theorem finsupp.update_eq_sub_add_single {α : Type u_1} {G : Type u_9} [add_group G] (f : α →₀ G) (a : α) (b : G) :
@[simp]
theorem finsupp.sum_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [has_zero M] [add_comm_monoid N] {f : α →₀ M} {g : α → M → β →₀ N} {a₂ : β} :
(f.sum g) a₂ = f.sum (λ (a₁ : α) (b : M), (g a₁ b) a₂)
theorem finsupp.support_sum {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [decidable_eq β] [has_zero M] [add_comm_monoid N] {f : α →₀ M} {g : α → M → β →₀ N} :
(f.sum g).support f.support.bUnion (λ (a : α), (g a (f a)).support)
theorem finsupp.support_finset_sum {α : Type u_1} {β : Type u_2} {M : Type u_5} [decidable_eq β] [add_comm_monoid M] {s : finset α} {f : α → β →₀ M} :
(s.sum f).support s.bUnion (λ (x : α), (f x).support)
@[simp]
theorem finsupp.sum_zero {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [add_comm_monoid N] {f : α →₀ M} :
f.sum (λ (a : α) (b : M), 0) = 0
@[simp]
theorem finsupp.sum_add {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [add_comm_monoid N] {f : α →₀ M} {h₁ h₂ : α → M → N} :
f.sum (λ (a : α) (b : M), h₁ a b + h₂ a b) = f.sum h₁ + f.sum h₂
@[simp]
theorem finsupp.prod_mul {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [comm_monoid N] {f : α →₀ M} {h₁ h₂ : α → M → N} :
f.prod (λ (a : α) (b : M), (h₁ a b) * h₂ a b) = (f.prod h₁) * f.prod h₂
@[simp]
theorem finsupp.prod_inv {α : Type u_1} {M : Type u_5} {G : Type u_9} [has_zero M] [comm_group G] {f : α →₀ M} {h : α → M → G} :
f.prod (λ (a : α) (b : M), (h a b)⁻¹) = (f.prod h)⁻¹
@[simp]
theorem finsupp.sum_neg {α : Type u_1} {M : Type u_5} {G : Type u_9} [has_zero M] [add_comm_group G] {f : α →₀ M} {h : α → M → G} :
f.sum (λ (a : α) (b : M), -h a b) = -f.sum h
@[simp]
theorem finsupp.sum_sub {α : Type u_1} {M : Type u_5} {G : Type u_9} [has_zero M] [add_comm_group G] {f : α →₀ M} {h₁ h₂ : α → M → G} :
f.sum (λ (a : α) (b : M), h₁ a b - h₂ a b) = f.sum h₁ - f.sum h₂
theorem finsupp.sum_add_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] {f g : α →₀ M} {h : α → M → N} (h_zero : ∀ (a : α), h a 0 = 0) (h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) :
(f + g).sum h = f.sum h + g.sum h
theorem finsupp.prod_add_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [comm_monoid N] {f g : α →₀ M} {h : α → M → N} (h_zero : ∀ (a : α), h a 0 = 1) (h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = (h a b₁) * h a b₂) :
(f + g).prod h = (f.prod h) * g.prod h
@[simp]
theorem finsupp.sum_add_index' {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] {f g : α →₀ M} (h : α → M →+ N) :
(f + g).sum (λ (x : α), (h x)) = f.sum (λ (x : α), (h x)) + g.sum (λ (x : α), (h x))
@[simp]
theorem finsupp.prod_add_index' {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid 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_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] :
(α → M →+ N) ≃+ ((α →₀ M) →+ N)

The canonical isomorphism between families of additive monoid homomorphisms α → (M →+ N) and monoid homomorphisms (α →₀ M) →+ N.

Equations
@[simp]
theorem finsupp.lift_add_hom_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (F : α → M →+ N) (f : α →₀ M) :
(finsupp.lift_add_hom F) f = f.sum (λ (x : α), (F x))
@[simp]
theorem finsupp.lift_add_hom_symm_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (F : →₀ M) →+ N) (x : α) :
theorem finsupp.lift_add_hom_symm_apply_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (F : →₀ M) →+ N) (x : α) (y : M) :
@[simp]
theorem finsupp.sum_single {α : Type u_1} {M : Type u_5} [add_comm_monoid M] (f : α →₀ M) :
@[simp]
theorem finsupp.lift_add_hom_apply_single {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (f : α → M →+ N) (a : α) (b : M) :
@[simp]
theorem finsupp.lift_add_hom_comp_single {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (f : α → M →+ N) (a : α) :
theorem finsupp.comp_lift_add_hom {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] (g : N →+ P) (f : α → M →+ N) :
theorem finsupp.sum_sub_index {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_group β] [add_comm_group γ] {f g : α →₀ β} {h : α → β → γ} (h_sub : ∀ (a : α) (b₁ b₂ : β), h a (b₁ - b₂) = h a b₁ - h a b₂) :
(f - g).sum h = f.sum h - g.sum h
theorem finsupp.sum_emb_domain {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [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_2} {M : Type u_5} {N : Type u_7} [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_4} {M : Type u_5} {N : Type u_7} [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₂) :
∏ (i : ι) in s, (g i).prod h = (∑ (i : ι) in s, g i).prod h
theorem finsupp.sum_finset_sum_index {α : Type u_1} {ι : Type u_4} {M : Type u_5} {N : Type u_7} [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₂) :
∑ (i : ι) in s, (g i).sum h = (∑ (i : ι) in s, g i).sum h
theorem finsupp.sum_sum_index {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} {P : Type u_8} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] {f : α →₀ M} {g : α → M → β →₀ N} {h : β → N → P} (h_zero : ∀ (a : β), h a 0 = 0) (h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂) :
(f.sum g).sum h = f.sum (λ (a : α) (b : M), (g a b).sum h)
theorem finsupp.prod_sum_index {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} {P : Type u_8} [add_comm_monoid M] [add_comm_monoid N] [comm_monoid P] {f : α →₀ M} {g : α → M → β →₀ N} {h : β → N → P} (h_zero : ∀ (a : β), h a 0 = 1) (h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = (h a b₁) * h a b₂) :
(f.sum g).prod h = f.prod (λ (a : α) (b : M), (g a b).prod h)
theorem finsupp.multiset_sum_sum_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (f : multiset →₀ M)) (h : α → M → N) (h₀ : ∀ (a : α), h a 0 = 0) (h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) :
f.sum.sum h = (multiset.map (λ (g : α →₀ M), g.sum h) f).sum
theorem finsupp.support_sum_eq_bUnion {α : Type u_1} {ι : Type u_2} {M : Type u_3} [add_comm_monoid M] {g : ι → α →₀ M} (s : finset ι) (h : ∀ (i₁ i₂ : ι), i₁ i₂disjoint (g i₁).support (g i₂).support) :
(∑ (i : ι) in s, g i).support = s.bUnion (λ (i : ι), (g i).support)
theorem finsupp.multiset_map_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [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.multiset_sum_sum {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [add_comm_monoid N] {f : α →₀ M} {h : α → M → multiset N} :
(f.sum h).sum = f.sum (λ (a : α) (b : M), (h a b).sum)
theorem finsupp.prod_add_index_of_disjoint {α : Type u_1} {M : Type u_5} [add_comm_monoid M] {f1 f2 : α →₀ M} (hd : disjoint f1.support f2.support) {β : Type u_2} [comm_monoid β] (g : α → M → β) :
(f1 + f2).prod g = (f1.prod g) * f2.prod g

For disjoint f1 and f2, and function g, the product of the products of g over f1 and f2 equals the product of g over f1 + f2

@[simp]
theorem finsupp.map_range.equiv_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [has_zero N] (f : M N) (hf : f 0 = 0) (hf' : (f.symm) 0 = 0) (g : α →₀ M) :
noncomputable def finsupp.map_range.equiv {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [has_zero N] (f : M N) (hf : f 0 = 0) (hf' : (f.symm) 0 = 0) :
→₀ M) →₀ N)

finsupp.map_range as an equiv.

Equations
@[simp]
theorem finsupp.map_range.equiv_refl {α : Type u_1} {M : Type u_5} [has_zero M] :
theorem finsupp.map_range.equiv_trans {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [has_zero M] [has_zero N] [has_zero P] (f : M N) (hf : f 0 = 0) (hf' : (f.symm) 0 = 0) (f₂ : N P) (hf₂ : f₂ 0 = 0) (hf₂' : (f₂.symm) 0 = 0) :
@[simp]
theorem finsupp.map_range.equiv_symm {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [has_zero N] (f : M N) (hf : f 0 = 0) (hf' : (f.symm) 0 = 0) :
noncomputable def finsupp.map_range.zero_hom {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [has_zero N] (f : zero_hom M N) :
zero_hom →₀ M) →₀ N)

Composition with a fixed zero-preserving homomorphism is itself an zero-preserving homomorphism on functions.

Equations
@[simp]
theorem finsupp.map_range.zero_hom_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [has_zero N] (f : zero_hom M N) (g : α →₀ M) :
@[simp]
theorem finsupp.map_range.zero_hom_id {α : Type u_1} {M : Type u_5} [has_zero M] :
theorem finsupp.map_range.zero_hom_comp {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [has_zero M] [has_zero N] [has_zero P] (f : zero_hom N P) (f₂ : zero_hom M N) :
noncomputable def finsupp.map_range.add_monoid_hom {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (f : M →+ N) :
→₀ M) →+ α →₀ N

Composition with a fixed additive homomorphism is itself an additive homomorphism on functions.

Equations
@[simp]
theorem finsupp.map_range.add_monoid_hom_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (f : M →+ N) (g : α →₀ M) :
theorem finsupp.map_range.add_monoid_hom_comp {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] (f : N →+ P) (f₂ : M →+ N) :
theorem finsupp.map_range_multiset_sum {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (f : M →+ N) (m : multiset →₀ M)) :
theorem finsupp.map_range_finset_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (f : M →+ N) (s : finset ι) (g : ι → α →₀ M) :
finsupp.map_range f _ (∑ (x : ι) in s, g x) = ∑ (x : ι) in s, finsupp.map_range f _ (g x)
noncomputable def finsupp.map_range.add_equiv {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (f : M ≃+ N) :
→₀ M) ≃+ →₀ N)

finsupp.map_range.add_monoid_hom as an equiv.

Equations
@[simp]
theorem finsupp.map_range.add_equiv_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (f : M ≃+ N) (g : α →₀ M) :
theorem finsupp.map_range.add_equiv_trans {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] (f : M ≃+ N) (f₂ : N ≃+ P) :
@[simp]
theorem finsupp.map_range.add_equiv_symm {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (f : M ≃+ N) :
@[simp]
theorem finsupp.map_range.add_equiv_to_equiv {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (f : M ≃+ N) :

Declarations about map_domain #

noncomputable def finsupp.map_domain {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (f : α → β) (v : α →₀ M) :
β →₀ M

Given f : α → β and v : α →₀ M, map_domain f v : β →₀ M is the finitely supported function whose value at a : β is the sum of v x over all x such that f x = a.

Equations
theorem finsupp.map_domain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] {f : α → β} (hf : function.injective f) (x : α →₀ M) (a : α) :
(finsupp.map_domain f x) (f a) = x a
theorem finsupp.map_domain_notin_range {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] {f : α → β} (x : α →₀ M) (a : β) (h : a set.range f) :
@[simp]
theorem finsupp.map_domain_id {α : Type u_1} {M : Type u_5} [add_comm_monoid M] {v : α →₀ M} :
theorem finsupp.map_domain_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [add_comm_monoid M] {v : α →₀ M} {f : α → β} {g : β → γ} :
@[simp]
theorem finsupp.map_domain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] {f : α → β} {a : α} {b : M} :
@[simp]
theorem finsupp.map_domain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] {f : α → β} :
theorem finsupp.map_domain_congr {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] {v : α →₀ M} {f g : α → β} (h : ∀ (x : α), x v.supportf x = g x) :
theorem finsupp.map_domain_add {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] {v₁ v₂ : α →₀ M} {f : α → β} :
@[simp]
theorem finsupp.map_domain_equiv_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] {f : α β} (x : α →₀ M) (a : β) :
@[simp]
theorem finsupp.map_domain.add_monoid_hom_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (f : α → β) (v : α →₀ M) :
noncomputable def finsupp.map_domain.add_monoid_hom {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (f : α → β) :
→₀ M) →+ β →₀ M

finsupp.map_domain is an add_monoid_hom.

Equations
theorem finsupp.map_domain.add_monoid_hom_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [add_comm_monoid M] (f : β → γ) (g : α → β) :
theorem finsupp.map_domain_finset_sum {α : Type u_1} {β : Type u_2} {ι : Type u_4} {M : Type u_5} [add_comm_monoid M] {f : α → β} {s : finset ι} {v : ι → α →₀ M} :
finsupp.map_domain f (∑ (i : ι) in s, v i) = ∑ (i : ι) in s, finsupp.map_domain f (v i)
theorem finsupp.map_domain_sum {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [has_zero N] {f : α → β} {s : α →₀ N} {v : α → N → α →₀ M} :
finsupp.map_domain f (s.sum v) = s.sum (λ (a : α) (b : N), finsupp.map_domain f (v a b))
theorem finsupp.map_domain_support {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] [decidable_eq β] {f : α → β} {s : α →₀ M} :
theorem finsupp.sum_map_domain_index {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] {f : α → β} {s : α →₀ M} {h : β → M → N} (h_zero : ∀ (b : β), h b 0 = 0) (h_add : ∀ (b : β) (m₁ m₂ : M), h b (m₁ + m₂) = h b m₁ + h b m₂) :
(finsupp.map_domain f s).sum h = s.sum (λ (a : α) (m : M), h (f a) m)
theorem finsupp.prod_map_domain_index {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [comm_monoid N] {f : α → β} {s : α →₀ M} {h : β → M → N} (h_zero : ∀ (b : β), h b 0 = 1) (h_add : ∀ (b : β) (m₁ m₂ : M), h b (m₁ + m₂) = (h b m₁) * h b m₂) :
(finsupp.map_domain f s).prod h = s.prod (λ (a : α) (m : M), h (f a) m)
@[simp]
theorem finsupp.sum_map_domain_index_add_monoid_hom {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] {f : α → β} {s : α →₀ M} (h : β → M →+ N) :
(finsupp.map_domain f s).sum (λ (b : β) (m : M), (h b) m) = s.sum (λ (a : α) (m : M), (h (f a)) m)

A version of sum_map_domain_index that takes a bundled add_monoid_hom, rather than separate linearity hypotheses.

theorem finsupp.emb_domain_eq_map_domain {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (f : α β) (v : α →₀ M) :
theorem finsupp.prod_map_domain_index_inj {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [comm_monoid N] {f : α → β} {s : α →₀ M} {h : β → M → N} (hf : function.injective f) :
(finsupp.map_domain f s).prod h = s.prod (λ (a : α) (b : M), h (f a) b)
theorem finsupp.sum_map_domain_index_inj {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] {f : α → β} {s : α →₀ M} {h : β → M → N} (hf : function.injective f) :
(finsupp.map_domain f s).sum h = s.sum (λ (a : α) (b : M), h (f a) b)
theorem finsupp.map_domain_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] {f : α → β} (hf : function.injective f) :
theorem finsupp.map_domain_map_range {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (f : α → β) (v : α →₀ M) (g : M → N) (h0 : g 0 = 0) (hadd : ∀ (x y : M), g (x + y) = g x + g y) :

When g preserves addition, map_range and map_domain commute.

Declarations about comap_domain #

noncomputable def finsupp.comap_domain {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α → β) (l : β →₀ M) (hf : set.inj_on f (f ⁻¹' (l.support))) :
α →₀ M

Given f : α → β, l : β →₀ M and a proof hf that f is injective on the preimage of l.support, comap_domain f l hf is the finitely supported function from α to M given by composing l with f.

Equations
@[simp]
theorem finsupp.comap_domain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α → β) (l : β →₀ M) (hf : set.inj_on f (f ⁻¹' (l.support))) (a : α) :
(finsupp.comap_domain f l hf) a = l (f a)
theorem finsupp.sum_comap_domain {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [has_zero M] [add_comm_monoid N] (f : α → β) (l : β →₀ M) (g : β → M → N) (hf : set.bij_on f (f ⁻¹' (l.support)) (l.support)) :
(finsupp.comap_domain f l _).sum (g f) = l.sum g
theorem finsupp.eq_zero_of_comap_domain_eq_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (f : α → β) (l : β →₀ M) (hf : set.bij_on f (f ⁻¹' (l.support)) (l.support)) :
finsupp.comap_domain f l _ = 0l = 0
theorem finsupp.map_domain_comap_domain {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (f : α → β) (l : β →₀ M) (hf : function.injective f) (hl : (l.support) set.range f) :
noncomputable def finsupp.some {α : Type u_1} {M : Type u_5} [has_zero M] (f : option α →₀ M) :
α →₀ M

Restrict a finitely supported function on option α to a finitely supported function on α.

Equations
@[simp]
theorem finsupp.some_apply {α : Type u_1} {M : Type u_5} [has_zero M] (f : option α →₀ M) (a : α) :
(f.some) a = f (some a)
@[simp]
theorem finsupp.some_zero {α : Type u_1} {M : Type u_5} [has_zero M] :
0.some = 0
@[simp]
theorem finsupp.some_add {α : Type u_1} {M : Type u_5} [add_comm_monoid M] (f g : option α →₀ M) :
(f + g).some = f.some + g.some
@[simp]
theorem finsupp.some_single_none {α : Type u_1} {M : Type u_5} [has_zero M] (m : M) :
@[simp]
theorem finsupp.some_single_some {α : Type u_1} {M : Type u_5} [has_zero M] (a : α) (m : M) :
theorem finsupp.prod_option_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [comm_monoid N] (f : option α →₀ M) (b : option αM → N) (h_zero : ∀ (o : option α), b o 0 = 1) (h_add : ∀ (o : option α) (m₁ m₂ : M), b o (m₁ + m₂) = (b o m₁) * b o m₂) :
f.prod b = (b none (f none)) * f.some.prod (λ (a : α), b (some a))
theorem finsupp.sum_option_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (f : option α →₀ M) (b : option αM → N) (h_zero : ∀ (o : option α), b o 0 = 0) (h_add : ∀ (o : option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ + b o m₂) :
f.sum b = b none (f none) + f.some.sum (λ (a : α), b (some a))
theorem finsupp.sum_option_index_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} [semiring R] [add_comm_monoid M] [module R M] (f : option α →₀ R) (b : option α → M) :
f.sum (λ (o : option α) (r : R), r b o) = f none b none + f.some.sum (λ (a : α) (r : R), r b (some a))

Declarations about equiv_congr_left #

def finsupp.equiv_map_domain {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (l : α →₀ M) :
β →₀ M

Given f : α ≃ β, we can map l : α →₀ M to equiv_map_domain f l : β →₀ M (computably) by mapping the support forwards and the function backwards.

Equations
@[simp]
theorem finsupp.equiv_map_domain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (l : α →₀ M) (b : β) :
theorem finsupp.equiv_map_domain_symm_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (l : β →₀ M) (a : α) :
@[simp]
theorem finsupp.equiv_map_domain_refl {α : Type u_1} {M : Type u_5} [has_zero M] (l : α →₀ M) :
theorem finsupp.equiv_map_domain_refl' {α : Type u_1} {M : Type u_5} [has_zero M] :
theorem finsupp.equiv_map_domain_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [has_zero M] (f : α β) (g : β γ) (l : α →₀ M) :
theorem finsupp.equiv_map_domain_trans' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [has_zero M] (f : α β) (g : β γ) :
@[simp]
theorem finsupp.equiv_map_domain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (a : α) (b : M) :
@[simp]
theorem finsupp.equiv_map_domain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] {f : α β} :
theorem finsupp.equiv_map_domain_eq_map_domain {α : Type u_1} {β : Type u_2} {M : Type u_3} [add_comm_monoid M] (f : α β) (l : α →₀ M) :
def finsupp.equiv_congr_left {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) :
→₀ M) →₀ M)

Given f : α ≃ β, the finitely supported function spaces are also in bijection: (α →₀ M) ≃ (β →₀ M).

This is the finitely-supported version of equiv.Pi_congr_left.

Equations
@[simp]
theorem finsupp.equiv_congr_left_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (l : α →₀ M) :
@[simp]
theorem finsupp.equiv_congr_left_symm {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) :

Declarations about filter #

noncomputable def finsupp.filter {α : Type u_1} {M : Type u_5} [has_zero M] (p : α → Prop) (f : α →₀ M) :
α →₀ M

filter p f is the function which is f a if p a is true and 0 otherwise.

Equations
theorem finsupp.filter_apply {α : Type u_1} {M : Type u_5} [has_zero M] (p : α → Prop) (f : α →₀ M) (a : α) [D : decidable (p a)] :
(finsupp.filter p f) a = ite (p a) (f a) 0
theorem finsupp.filter_eq_indicator {α : Type u_1} {M : Type u_5} [has_zero M] (p : α → Prop) (f : α →₀ M) :
(finsupp.filter p f) = {x : α | p x}.indicator f
@[simp]
theorem finsupp.filter_apply_pos {α : Type u_1} {M : Type u_5} [has_zero M] (p : α → Prop) (f : α →₀ M) {a : α} (h : p a) :
@[simp]
theorem finsupp.filter_apply_neg {α : Type u_1} {M : Type u_5} [has_zero M] (p : α → Prop) (f : α →₀ M) {a : α} (h : ¬p a) :
@[simp]
theorem finsupp.support_filter {α : Type u_1} {M : Type u_5} [has_zero M] (p : α → Prop) (f : α →₀ M) [D : decidable_pred p] :
theorem finsupp.filter_zero {α : Type u_1} {M : Type u_5} [has_zero M] (p : α → Prop) :
@[simp]
theorem finsupp.filter_single_of_pos {α : Type u_1} {M : Type u_5} [has_zero M] (p : α → Prop) {a : α} {b : M} (h : p a) :
@[simp]
theorem finsupp.filter_single_of_neg {α : Type u_1} {M : Type u_5} [has_zero M] (p : α → Prop) {a : α} {b : M} (h : ¬p a) :
theorem finsupp.filter_pos_add_filter_neg {α : Type u_1} {M : Type u_5} [add_zero_class M] (f : α →₀ M) (p : α → Prop) :
finsupp.filter p f + finsupp.filter (λ (a : α), ¬p a) f = f

Declarations about frange #

noncomputable def finsupp.frange {α : Type u_1} {M : Type u_5} [has_zero M] (f : α →₀ M) :

frange f is the image of f on the support of f.

Equations
theorem finsupp.mem_frange {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} {y : M} :
y f.frange y 0 ∃ (x : α), f x = y
theorem finsupp.zero_not_mem_frange {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} :
theorem finsupp.frange_single {α : Type u_1} {M : Type u_5} [has_zero M] {x : α} {y : M} :

Declarations about subtype_domain #

noncomputable def finsupp.subtype_domain {α : Type u_1} {M : Type u_5} [has_zero M] (p : α → Prop) (f : α →₀ M) :

subtype_domain p f is the restriction of the finitely supported function f to the subtype p.

Equations
@[simp]
theorem finsupp.support_subtype_domain {α : Type u_1} {M : Type u_5} [has_zero M] {p : α → Prop} [D : decidable_pred p] {f : α →₀ M} :
@[simp]
theorem finsupp.subtype_domain_apply {α : Type u_1} {M : Type u_5} [has_zero M] {p : α → Prop} {a : subtype p} {v : α →₀ M} :
@[simp]
theorem finsupp.subtype_domain_zero {α : Type u_1} {M : Type u_5} [has_zero M] {p : α → Prop} :
theorem finsupp.subtype_domain_eq_zero_iff' {α : Type u_1} {M : Type u_5} [has_zero M] {p : α → Prop} {f : α →₀ M} :
finsupp.subtype_domain p f = 0 ∀ (x : α), p xf x = 0
theorem finsupp.subtype_domain_eq_zero_iff {α : Type u_1} {M : Type u_5} [has_zero M] {p : α → Prop} {f : α →₀ M} (hf : ∀ (x : α), x f.supportp x) :
theorem finsupp.sum_subtype_domain_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] {p : α → Prop} [add_comm_monoid N] {v : α →₀ M} {h : α → M → N} (hp : ∀ (x : α), x v.supportp x) :
(finsupp.subtype_domain p v).sum (λ (a : subtype p) (b : M), h a b) = v.sum h
theorem finsupp.prod_subtype_domain_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] {p : α → Prop} [comm_monoid N] {v : α →₀ M} {h : α → M → N} (hp : ∀ (x : α), x v.supportp x) :
(finsupp.subtype_domain p v).prod (λ (a : subtype p) (b : M), h a b) = v.prod h
@[simp]
theorem finsupp.subtype_domain_add {α : Type u_1} {M : Type u_5} [add_zero_class M] {p : α → Prop} {v v' : α →₀ M} :
noncomputable def finsupp.subtype_domain_add_monoid_hom {α : Type u_1} {M : Type u_5} [add_zero_class M] {p : α → Prop} :

subtype_domain but as an add_monoid_hom.

Equations
noncomputable def finsupp.filter_add_hom {α : Type u_1} {M : Type u_5} [add_zero_class M] (p : α → Prop) :
→₀ M) →+ α →₀ M

finsupp.filter as an add_monoid_hom.

Equations
@[simp]
theorem finsupp.filter_add {α : Type u_1} {M : Type u_5} [add_zero_class M] {p : α → Prop} {v v' : α →₀ M} :
theorem finsupp.subtype_domain_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} [add_comm_monoid M] {p : α → Prop} {s : finset ι} {h : ι → α →₀ M} :
finsupp.subtype_domain p (∑ (c : ι) in s, h c) = ∑ (c : ι) in s, finsupp.subtype_domain p (h c)
theorem finsupp.subtype_domain_finsupp_sum {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] {p : α → Prop} [has_zero N] {s : β →₀ N} {h : β → N → α →₀ M} :
finsupp.subtype_domain p (s.sum h) = s.sum (λ (c : β) (d : N), finsupp.subtype_domain p (h c d))
theorem finsupp.filter_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} [add_comm_monoid M] {p : α → Prop} (s : finset ι) (f : ι → α →₀ M) :
finsupp.filter p (∑ (a : ι) in s, f a) = ∑ (a : ι) in s, finsupp.filter p (f a)
theorem finsupp.filter_eq_sum {α : Type u_1} {M : Type u_5} [add_comm_monoid M] (p : α → Prop) [D : decidable_pred p] (f : α →₀ M) :
finsupp.filter p f = ∑ (i : α) in finset.filter p f.support, finsupp.single i (f i)
@[simp]
theorem finsupp.subtype_domain_neg {α : Type u_1} {G : Type u_9} [add_group G] {p : α → Prop} {v : α →₀ G} :
@[simp]
theorem finsupp.subtype_domain_sub {α : Type u_1} {G : Type u_9} [add_group G] {p : α → Prop} {v v' : α →₀ G} :
@[simp]
theorem finsupp.single_neg {α : Type u_1} {G : Type u_9} [add_group G] {a : α} {b : G} :
@[simp]
theorem finsupp.single_sub {α : Type u_1} {G : Type u_9} [add_group G] {a : α} {b₁ b₂ : G} :
finsupp.single a (b₁ - b₂) = finsupp.single a b₁ - finsupp.single a b₂
@[simp]
theorem finsupp.erase_neg {α : Type u_1} {G : Type u_9} [add_group G] (a : α) (f : α →₀ G) :
@[simp]
theorem finsupp.erase_sub {α : Type u_1} {G : Type u_9} [add_group G] (a : α) (f₁ f₂ : α →₀ G) :
finsupp.erase a (f₁ - f₂) = finsupp.erase a f₁ - finsupp.erase a f₂
@[simp]
theorem finsupp.filter_neg {α : Type u_1} {G : Type u_9} [add_group G] (p : α → Prop) (f : α →₀ G) :
@[simp]
theorem finsupp.filter_sub {α : Type u_1} {G : Type u_9} [add_group G] (p : α → Prop) (f₁ f₂ : α →₀ G) :
finsupp.filter p (f₁ - f₂) = finsupp.filter p f₁ - finsupp.filter p f₂

Declarations relating finsupp to multiset #

noncomputable def finsupp.to_multiset {α : Type u_1} :

Given f : α →₀ ℕ, f.to_multiset is the multiset with multiplicities given by the values of f on the elements of α. We define this function as an add_equiv.

Equations
theorem finsupp.to_multiset_zero {α : Type u_1} :
theorem finsupp.to_multiset_apply {α : Type u_1} (f : α →₀ ) :
finsupp.to_multiset f = f.sum (λ (a : α) (n : ), n {a})
@[simp]
theorem finsupp.to_multiset_symm_apply {α : Type u_1} [decidable_eq α] (s : multiset α) (x : α) :
@[simp]
theorem finsupp.to_multiset_single {α : Type u_1} (a : α) (n : ) :
theorem finsupp.to_multiset_sum {α : Type u_1} {ι : Type u_2} {f : ι → α →₀ } (s : finset ι) :
finsupp.to_multiset (∑ (i : ι) in s, f i) = ∑ (i : ι) in s, finsupp.to_multiset (f i)
theorem finsupp.to_multiset_sum_single {ι : Type u_1} (s : finset ι) (n : ) :
finsupp.to_multiset (∑ (i : ι) in s, finsupp.single i n) = n s.val
theorem finsupp.card_to_multiset {α : Type u_1} (f : α →₀ ) :
theorem finsupp.to_multiset_map {α : Type u_1} {β : Type u_2} (f : α →₀ ) (g : α → β) :
@[simp]
theorem finsupp.prod_to_multiset {M : Type u_5} [comm_monoid M] (f : M →₀ ) :
(finsupp.to_multiset f).prod = f.prod (λ (a : M) (n : ), a ^ n)
@[simp]
@[simp]
theorem finsupp.count_to_multiset {α : Type u_1} [decidable_eq α] (f : α →₀ ) (a : α) :
theorem finsupp.mem_support_multiset_sum {α : Type u_1} {M : Type u_5} [add_comm_monoid M] {s : multiset →₀ M)} (a : α) :
a s.sum.support(∃ (f : α →₀ M) (H : f s), a f.support)
theorem finsupp.mem_support_finset_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} [add_comm_monoid M] {s : finset ι} {h : ι → α →₀ M} (a : α) (ha : a (∑ (c : ι) in s, h c).support) :
∃ (c : ι) (H : c s), a (h c).support
@[simp]
theorem finsupp.mem_to_multiset {α : Type u_1} (f : α →₀ ) (i : α) :

Declarations about curry and uncurry #

@[protected]
noncomputable def finsupp.curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (f : α × β →₀ M) :
α →₀ β →₀ M

Given a finitely supported function f from a product type α × β to γ, curry f is the "curried" finitely supported function from α to the type of finitely supported functions from β to γ.

Equations
@[simp]
theorem finsupp.curry_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (f : α × β →₀ M) (x : α) (y : β) :
((f.curry) x) y = f (x, y)
theorem finsupp.sum_curry_index {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (f : α × β →₀ M) (g : α → β → M → N) (hg₀ : ∀ (a : α) (b : β), g a b 0 = 0) (hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁) :
f.curry.sum (λ (a : α) (f : β →₀ M), f.sum (g a)) = f.sum (λ (p : α × β) (c : M), g p.fst p.snd c)
@[protected]
noncomputable def finsupp.uncurry {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (f : α →₀ β →₀ M) :
α × β →₀ M

Given a finitely supported function f from α to the type of finitely supported functions from β to M, uncurry f is the "uncurried" finitely supported function from α × β to M.

Equations
noncomputable def finsupp.finsupp_prod_equiv {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] :
× β →₀ M) →₀ β →₀ M)

finsupp_prod_equiv defines the equiv between ((α × β) →₀ M) and (α →₀ (β →₀ M)) given by currying and uncurrying.

Equations
theorem finsupp.filter_curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (f : α × β →₀ M) (p : α → Prop) :
(finsupp.filter (λ (a : α × β), p a.fst) f).curry = finsupp.filter p f.curry
theorem finsupp.support_curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] [decidable_eq α] (f : α × β →₀ M) :
noncomputable def finsupp.sum_elim {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (f : α →₀ γ) (g : β →₀ γ) :
α β →₀ γ

finsupp.sum_elim f g maps inl x to f x and inr y to g y.

Equations
@[simp]
theorem finsupp.coe_sum_elim {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (f : α →₀ γ) (g : β →₀ γ) :
theorem finsupp.sum_elim_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (f : α →₀ γ) (g : β →₀ γ) (x : α β) :
theorem finsupp.sum_elim_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (f : α →₀ γ) (g : β →₀ γ) (x : α) :
(f.sum_elim g) (sum.inl x) = f x
theorem finsupp.sum_elim_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (f : α →₀ γ) (g : β →₀ γ) (x : β) :
(f.sum_elim g) (sum.inr x) = g x
@[simp]
theorem finsupp.sum_finsupp_equiv_prod_finsupp_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (fg : →₀ γ) × →₀ γ)) :
noncomputable def finsupp.sum_finsupp_equiv_prod_finsupp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] :
β →₀ γ) →₀ γ) × →₀ γ)

The equivalence between (α ⊕ β) →₀ γ and (α →₀ γ) × (β →₀ γ).

This is the finsupp version of equiv.sum_arrow_equiv_prod_arrow.

Equations
@[simp]
theorem finsupp.fst_sum_finsupp_equiv_prod_finsupp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (f : α β →₀ γ) (x : α) :
theorem finsupp.snd_sum_finsupp_equiv_prod_finsupp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (f : α β →₀ γ) (y : β) :
theorem finsupp.sum_finsupp_equiv_prod_finsupp_symm_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (fg : →₀ γ) × →₀ γ)) (x : α) :
theorem finsupp.sum_finsupp_equiv_prod_finsupp_symm_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (fg : →₀ γ) × →₀ γ)) (y : β) :
noncomputable def finsupp.sum_finsupp_add_equiv_prod_finsupp {M : Type u_5} [add_monoid M] {α : Type u_1} {β : Type u_2} :
β →₀ M) ≃+ →₀ M) × →₀ M)

The additive equivalence between (α ⊕ β) →₀ M and (α →₀ M) × (β →₀ M).

This is the finsupp version of equiv.sum_arrow_equiv_prod_arrow.

Equations
theorem finsupp.fst_sum_finsupp_add_equiv_prod_finsupp {M : Type u_5} [add_monoid M] {α : Type u_1} {β : Type u_2} (f : α β →₀ M) (x : α) :
theorem finsupp.snd_sum_finsupp_add_equiv_prod_finsupp {M : Type u_5} [add_monoid M] {α : Type u_1} {β : Type u_2} (f : α β →₀ M) (y : β) :
theorem finsupp.sum_finsupp_add_equiv_prod_finsupp_symm_inl {M : Type u_5} [add_monoid M] {α : Type u_1} {β : Type u_2} (fg : →₀ M) × →₀ M)) (x : α) :
theorem finsupp.sum_finsupp_add_equiv_prod_finsupp_symm_inr {M : Type u_5} [add_monoid M] {α : Type u_1} {β : Type u_2} (fg : →₀ M) × →₀ M)) (y : β) :
noncomputable def finsupp.comap_has_scalar {α : Type u_1} {M : Type u_5} {G : Type u_9} [group G] [mul_action G α] [add_comm_monoid M] :

Scalar multiplication by a group element g, given by precomposition with the action of g⁻¹ on the domain.

Equations
noncomputable def finsupp.comap_mul_action {α : Type u_1} {M : Type u_5} {G : Type u_9} [group G] [mul_action G α] [add_comm_monoid M] :

Scalar multiplication by a group element, given by precomposition with the action of g⁻¹ on the domain, is multiplicative in g.

Equations
noncomputable def finsupp.comap_distrib_mul_action {α : Type u_1} {M : Type u_5} {G : Type u_9} [group G] [mul_action G α] [add_comm_monoid M] :

Scalar multiplication by a group element, given by precomposition with the action of g⁻¹ on the domain, is additive in the second argument.

Equations
noncomputable def finsupp.comap_distrib_mul_action_self {M : Type u_5} {G : Type u_9} [group G] [add_comm_monoid M] :

Scalar multiplication by a group element on finitely supported functions on a group, given by precomposition with the action of g⁻¹.

Equations
@[simp]
theorem finsupp.comap_smul_single {α : Type u_1} {M : Type u_5} {G : Type u_9} [group G] [mul_action G α] [add_comm_monoid M] (g : G) (a : α) (b : M) :
@[simp]
theorem finsupp.comap_smul_apply {α : Type u_1} {M : Type u_5} {G : Type u_9} [group G] [mul_action G α] [add_comm_monoid M] (g : G) (f : α →₀ M) (a : α) :
(g f) a = f (g⁻¹ a)
@[protected, instance]
noncomputable def finsupp.has_scalar {α : Type u_1} {M : Type u_5} {R : Type u_11} [monoid R] [add_monoid M] [distrib_mul_action R M] :
Equations

Throughout this section, some monoid and semiring arguments are specified with {} instead of []. See note [implicit instance arguments].

@[simp]
theorem finsupp.coe_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} {_x : monoid R} [add_monoid M] [distrib_mul_action R M] (b : R) (v : α →₀ M) :
(b v) = b v
theorem finsupp.smul_apply {α : Type u_1} {M : Type u_5} {R : Type u_11} {_x : monoid R} [add_monoid M] [distrib_mul_action R M] (b : R) (v : α →₀ M) (a : α) :
(b v) a = b v a
theorem is_smul_regular.finsupp {α : Type u_1} {M : Type u_5} {R : Type u_11} {_x : monoid R} [add_monoid M] [distrib_mul_action R M] {k : R} (hk : is_smul_regular M k) :
@[protected, instance]
def finsupp.has_faithful_scalar {α : Type u_1} {M : Type u_5} {R : Type u_11} [monoid R] [nonempty α] [add_monoid M] [distrib_mul_action R M] [has_faithful_scalar R M] :
@[protected, instance]
noncomputable def finsupp.distrib_mul_action (α : Type u_1) (M : Type u_5) {R : Type u_11} [monoid R] [add_monoid M] [distrib_mul_action R M] :
Equations
@[protected, instance]
def finsupp.is_scalar_tower (α : Type u_1) (M : Type u_5) {R : Type u_11} {S : Type u_12} [monoid R] [monoid S] [add_monoid M] [distrib_mul_action R M] [distrib_mul_action S M] [has_scalar R S] [is_scalar_tower R S M] :
@[protected, instance]
def finsupp.smul_comm_class (α : Type u_1) (M : Type u_5) {R : Type u_11} {S : Type u_12} [monoid R] [monoid S] [add_monoid M] [distrib_mul_action R M] [distrib_mul_action S M] [smul_comm_class R S M] :
@[protected, instance]
def finsupp.is_central_scalar (α : Type u_1) (M : Type u_5) {R : Type u_11} [monoid R] [add_monoid M] [distrib_mul_action R M] [distrib_mul_action Rᵐᵒᵖ M] [is_central_scalar R M] :
@[protected, instance]
noncomputable def finsupp.module (α : Type u_1) (M : Type u_5) {R : Type u_11} [semiring R] [add_comm_monoid M] [module R M] :
module R →₀ M)
Equations
theorem finsupp.support_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} {_x : monoid R} [add_monoid M] [distrib_mul_action R M] {b : R} {g : α →₀ M} :
@[simp]
theorem finsupp.filter_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} {p : α → Prop} {_x : monoid R} [add_monoid M] [distrib_mul_action R M] {b : R} {v : α →₀ M} :
theorem finsupp.map_domain_smul {α : Type u_1} {β : Type u_2} {M : Type u_5} {R : Type u_11} {_x : monoid R} [add_comm_monoid M] [distrib_mul_action R M] {f : α → β} (b : R) (v : α →₀ M) :
@[simp]
theorem finsupp.smul_single {α : Type u_1} {M : Type u_5} {R : Type u_11} {_x : monoid R} [add_monoid M] [distrib_mul_action R M] (c : R) (a : α) (b : M) :
@[simp]
theorem finsupp.smul_single' {α : Type u_1} {R : Type u_11} {_x : semiring R} (c : R) (a : α) (b : R) :
theorem finsupp.map_range_smul {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} {_x : monoid R} [add_monoid M] [distrib_mul_action R M] [add_monoid N] [distrib_mul_action R N] {f : M → N} {hf : f 0 = 0} (c : R) (v : α →₀ M) (hsmul : ∀ (x : M), f (c x) = c f x) :
theorem finsupp.smul_single_one {α : Type u_1} {R : Type u_11} [semiring R] (a : α) (b : R) :
theorem finsupp.sum_smul_index {α : Type u_1} {M : Type u_5} {R : Type u_11} [semiring R] [add_comm_monoid M] {g : α →₀ R} {b : R} {h : α → R → M} (h0 : ∀ (i : α), h i 0 = 0) :
(b g).sum h = g.sum (λ (i : α) (a : R), h i (b * a))
theorem finsupp.sum_smul_index' {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} [monoid R] [add_monoid M] [distrib_mul_action R M] [add_comm_monoid N] {g : α →₀ M} {b : R} {h : α → M → N} (h0 : ∀ (i : α), h i 0 = 0) :
(b g).sum h = g.sum (λ (i : α) (c : M), h i (b c))
theorem finsupp.sum_smul_index_add_monoid_hom {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} [monoid R] [add_monoid M] [add_comm_monoid N] [distrib_mul_action R M] {g : α →₀ M} {b : R} {h : α → M →+ N} :
(b g).sum (λ (a : α), (h a)) = g.sum (λ (i : α) (c : M), (h i) (b c))

A version of finsupp.sum_smul_index' for bundled additive maps.

@[protected, instance]
def finsupp.no_zero_smul_divisors {M : Type u_5} {R : Type u_11} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_1} [no_zero_smul_divisors R M] :
noncomputable def finsupp.distrib_mul_action_hom.single {α : Type u_1} {M : Type u_5} {R : Type u_11} [semiring R] [add_comm_monoid M] [distrib_mul_action R M] (a : α) :
M →+[R] α →₀ M

finsupp.single as a distrib_mul_action_hom.

See also finsupp.lsingle for the version as a linear map.

Equations
theorem finsupp.distrib_mul_action_hom_ext {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} [semiring R] [add_comm_monoid M] [add_comm_monoid N] [distrib_mul_action R M] [distrib_mul_action R N] {f g : →₀ M) →+[R] N} (h : ∀ (a : α) (m : M), f (finsupp.single a m) = g (finsupp.single a m)) :
f = g
@[ext]
theorem finsupp.distrib_mul_action_hom_ext' {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} [semiring R] [add_comm_monoid M] [add_comm_monoid N] [distrib_mul_action R M] [distrib_mul_action R N] {f g : →₀ M) →+[R] N} (h : ∀ (a : α), f.comp (finsupp.distrib_mul_action_hom.single a) = g.comp (finsupp.distrib_mul_action_hom.single a)) :
f = g

See note [partially-applied ext lemmas].

@[protected, instance]
def finsupp.unique_of_right {α : Type u_1} {R : Type u_11} [has_zero R] [subsingleton R] :
unique →₀ R)

The finsupp version of pi.unique.

Equations
@[protected, instance]
def finsupp.unique_of_left {α : Type u_1} {R : Type u_11} [has_zero R] [is_empty α] :
unique →₀ R)

The finsupp version of pi.unique_of_is_empty.

Equations
noncomputable def finsupp.restrict_support_equiv {α : Type u_1} (s : set α) (M : Type u_2) [add_comm_monoid M] :
{f // (f.support) s} (s →₀ M)

Given an add_comm_monoid M and s : set α, restrict_support_equiv s M is the equiv between the subtype of finitely supported functions with support contained in s and the type of finitely supported functions from s.

Equations
@[simp]
theorem finsupp.dom_congr_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (e : α β) (l : α →₀ M) :
@[protected]
noncomputable def finsupp.dom_congr {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (e : α β) :
→₀ M) ≃+ →₀ M)

Given add_comm_monoid M and e : α ≃ β, dom_congr e is the corresponding equiv between α →₀ M and β →₀ M.

This is finsupp.equiv_congr_left as an add_equiv.

Equations
@[simp]
theorem finsupp.dom_congr_refl {α : Type u_1} {M : Type u_5} [add_comm_monoid M] :
@[simp]
theorem finsupp.dom_congr_symm {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (e : α β) :
@[simp]
theorem finsupp.dom_congr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [add_comm_monoid M] (e : α β) (f : β γ) :

Declarations about sigma types #

noncomputable def finsupp.split {ι : Type u_4} {M : Type u_5} {αs : ι → Type u_13} [has_zero M] (l : (Σ (i : ι), αs i) →₀ M) (i : ι) :
αs i →₀ M

Given l, a finitely supported function from the sigma type Σ (i : ι), αs i to M and an index element i : ι, split l i is the ith component of l, a finitely supported function from as i to M.

This is the finsupp version of sigma.curry.

Equations
theorem finsupp.split_apply {ι : Type u_4} {M : Type u_5} {αs : ι → Type u_13} [has_zero M] (l : (Σ (i : ι), αs i) →₀ M) (i : ι) (x : αs i) :
(l.split i) x = l i, x⟩
noncomputable def finsupp.split_support {ι : Type u_4} {M : Type u_5} {αs : ι → Type u_13} [has_zero M] (l : (Σ (i : ι), αs i) →₀ M) :

Given l, a finitely supported function from the sigma type Σ (i : ι), αs i to β, split_support l is the finset of indices in ι that appear in the support of l.

Equations
theorem finsupp.mem_split_support_iff_nonzero {ι : Type u_4} {M : Type u_5} {αs : ι → Type u_13} [has_zero M] (l : (Σ (i : ι), αs i) →₀ M) (i : ι) :
noncomputable def finsupp.split_comp {ι : Type u_4} {M : Type u_5} {N : Type u_7} {αs : ι → Type u_13} [has_zero M] (l : (Σ (i : ι), αs i) →₀ M) [has_zero N] (g : Π (i : ι), (αs i →₀ M) → N) (hg : ∀ (i : ι) (x : αs i →₀ M), x = 0 g i x = 0) :
ι →₀ N

Given l, a finitely supported function from the sigma type Σ i, αs i to β and an ι-indexed family g of functions from (αs i →₀ β) to γ, split_comp defines a finitely supported function from the index type ι to γ given by composing g i with split l i.

Equations
theorem finsupp.sigma_support {ι : Type u_4} {M : Type u_5} {αs : ι → Type u_13} [has_zero M] (l : (Σ (i : ι), αs i) →₀ M) :
l.support = l.split_support.sigma (λ (i : ι), (l.split i).support)
theorem finsupp.sigma_sum {ι : Type u_4} {M : Type u_5} {N : Type u_7} {αs : ι → Type u_13} [has_zero M] (l : (Σ (i : ι), αs i) →₀ M) [add_comm_monoid N] (f : (Σ (i : ι), αs i)M → N) :
l.sum f = ∑ (i : ι) in l.split_support, (l.split i).sum (λ (a : αs i) (b : M), f i, a⟩ b)
noncomputable def finsupp.sigma_finsupp_equiv_pi_finsupp {α : Type u_1} {η : Type u_14} [fintype η] {ιs : η → Type u_15} [has_zero α] :
((Σ (j : η), ιs j) →₀ α) Π (j : η), ιs j →₀ α

On a fintype η, finsupp.split is an equivalence between (Σ (j : η), ιs j) →₀ α and Π j, (ιs j →₀ α).

This is the finsupp version of equiv.Pi_curry.

Equations
@[simp]
theorem finsupp.sigma_finsupp_equiv_pi_finsupp_apply {α : Type u_1} {η : Type u_14} [fintype η] {ιs : η → Type u_15} [has_zero α] (f : (Σ (j : η), ιs j) →₀ α) (j : η) (i : ιs j) :
noncomputable def finsupp.sigma_finsupp_add_equiv_pi_finsupp {η : Type u_14} [fintype η] {α : Type u_1} {ιs : η → Type u_2} [add_monoid α] :
((Σ (j : η), ιs j) →₀ α) ≃+ Π (j : η), ιs j →₀ α

On a fintype η, finsupp.split is an additive equivalence between (Σ (j : η), ιs j) →₀ α and Π j, (ιs j →₀ α).

This is the add_equiv version of finsupp.sigma_finsupp_equiv_pi_finsupp.

Equations
@[simp]
theorem finsupp.sigma_finsupp_add_equiv_pi_finsupp_apply {η : Type u_14} [fintype η] {α : Type u_1} {ιs : η → Type u_2} [add_monoid α] (f : (Σ (j : η), ιs j) →₀ α) (j : η) (i : ιs j) :

Declarations relating multiset to finsupp #

noncomputable def multiset.to_finsupp {α : Type u_1} :

Given a multiset s, s.to_finsupp returns the finitely supported function on given by the multiplicities of the elements of s.

Equations
@[simp]
theorem multiset.to_finsupp_support {α : Type u_1} [D : decidable_eq α] (s : multiset α) :
@[simp]
theorem multiset.to_finsupp_apply {α : Type u_1} [D : decidable_eq α] (s : multiset α) (a : α) :
theorem multiset.to_finsupp_zero {α : Type u_1} :
@[simp]
theorem multiset.to_finsupp_singleton {α : Type u_1} (a : α) :

Declarations about order(ed) instances on finsupp #

@[protected, instance]
def finsupp.preorder {α : Type u_1} {M : Type u_5} [preorder M] [has_zero M] :
Equations
@[protected, instance]
def finsupp.partial_order {α : Type u_1} {M : Type u_5} [partial_order M] [has_zero M] :
Equations
theorem finsupp.le_def {α : Type u_1} {M : Type u_5} [preorder M] [has_zero M] {f g : α →₀ M} :
f g ∀ (x : α), f x g x
theorem finsupp.le_iff' {α : Type u_1} {M : Type u_5} [canonically_ordered_add_monoid M] (f g : α →₀ M) {t : finset α} (hf : f.support t) :
f g ∀ (s : α), s tf s g s
theorem finsupp.le_iff {α : Type u_1} {M : Type u_5} [canonically_ordered_add_monoid M] (f g : α →₀ M) :
f g ∀ (s : α), s f.supportf s g s
@[protected, instance]
Equations
@[simp]
theorem finsupp.single_le_iff {α : Type u_1} {M : Type u_5} [canonically_ordered_add_monoid M] {i : α} {x : M} {f : α →₀ M} :
@[simp]
theorem finsupp.add_eq_zero_iff {α : Type u_1} {M : Type u_5} [canonically_ordered_add_monoid M] (f g : α →₀ M) :
f + g = 0 f = 0 g = 0
noncomputable def finsupp.order_iso_multiset {α : Type u_1} :

finsupp.to_multiset as an order isomorphism.

Equations
theorem finsupp.sum_id_lt_of_lt {α : Type u_1} (m n : α →₀ ) (h : m < n) :
m.sum (λ (_x : α), id) < n.sum (λ (_x : α), id)
theorem finsupp.lt_wf (α : Type u_1) :

The order on σ →₀ ℕ is well-founded.

Declarations about subtraction on finsupp with codomain a canonically_ordered_add_monoid.

Some of these lemmas are used to develop the partial derivative on mv_polynomial.

@[protected, instance]
def finsupp.order_bot {α : Type u_1} {M : Type u_5} [canonically_ordered_add_monoid M] :
Equations
@[protected, instance]
noncomputable def finsupp.tsub {α : Type u_1} {M : Type u_5} [canonically_ordered_add_monoid M] [has_sub M] [has_ordered_sub M] :

This is called tsub for truncated subtraction, to distinguish it with subtraction in an additive group.

Equations
@[simp]
theorem finsupp.coe_tsub {α : Type u_1} {M : Type u_5} [canonically_ordered_add_monoid M] [has_sub M] [has_ordered_sub M] (g₁ g₂ : α →₀ M) :
(g₁ - g₂) = g₁ - g₂
theorem finsupp.tsub_apply {α : Type u_1} {M : Type u_5} [canonically_ordered_add_monoid M] [has_sub M] [has_ordered_sub M] (g₁ g₂ : α →₀ M) (a : α) :
(g₁ - g₂) a = g₁ a - g₂ a
@[protected, instance]
noncomputable def finsupp.has_ordered_sub {α : Type u_1} {M : Type u_5} [canonically_ordered_add_monoid M] [has_sub M] [has_ordered_sub M] :
Equations
@[simp]
theorem finsupp.single_tsub {α : Type u_1} {M : Type u_5} [canonically_ordered_add_monoid M] [has_sub M] [has_ordered_sub M] {a : α} {n₁ n₂ : M} :
finsupp.single a (n₁ - n₂) = finsupp.single a n₁ - finsupp.single a n₂
theorem finsupp.support_tsub {α : Type u_1} {M : Type u_5} [canonically_ordered_add_monoid M] [has_sub M] [has_ordered_sub M] {f1 f2 : α →₀ M} :
(f1 - f2).support f1.support
theorem finsupp.subset_support_tsub {α : Type u_1} {M : Type u_5} [canonically_ordered_add_monoid M] [has_sub M] [has_ordered_sub M] {f1 f2 : α →₀ M} :
f1.support \ f2.support (f1 - f2).support

Some lemmas specifically about .

theorem finsupp.sub_single_one_add {α : Type u_1} {a : α} {u u' : α →₀ } (h : u a 0) :
u - finsupp.single a 1 + u' = u + u' - finsupp.single a 1
theorem finsupp.add_sub_single_one {α : Type u_1} {a : α} {u u' : α →₀ } (h : u' a 0) :
u + (u' - finsupp.single a 1) = u + u' - finsupp.single a 1
@[simp, norm_cast]
theorem nat.cast_finsupp_prod {α : Type u_1} {M : Type u_5} {R : Type u_11} [has_zero M] (f : α →₀ M) [comm_semiring R] (g : α → M → ) :
(f.prod g) = f.prod (λ (a : α) (b : M), (g a b))
@[simp, norm_cast]
theorem nat.cast_finsupp_sum {α : Type u_1} {M : Type u_5} {R : Type u_11} [has_zero M] (f : α →₀ M) [comm_semiring R] (g : α → M → ) :
(f.sum g) = f.sum (λ (a : α) (b : M), (g a b))
@[simp, norm_cast]
theorem int.cast_finsupp_prod {α : Type u_1} {M : Type u_5} {R : Type u_11} [has_zero M] (f : α →₀ M) [comm_ring R] (g : α → M → ) :
(f.prod g) = f.prod (λ (a : α) (b : M), (g a b))
@[simp, norm_cast]
theorem int.cast_finsupp_sum {α : Type u_1} {M : Type u_5} {R : Type u_11} [has_zero M] (f : α →₀ M) [comm_ring R] (g : α → M → ) :
(f.sum g) = f.sum (λ (a : α) (b : M), (g a b))