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

@[instance]
def finsupp.has_coe_to_fun {α : Type u_1} {M : Type u_5} [has_zero 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) :

@[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 = λ (_x : α), 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] :

@[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

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.injective_coe_fn {α : Type u_1} {M : Type u_5} [has_zero M] :
function.injective (show →₀ M)α → M, from coe_fn)

@[ext]
theorem finsupp.ext {α : Type u_1} {M : Type u_5} [has_zero M] {f g : α →₀ M} :
(∀ (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

@[simp]
theorem finsupp.support_eq_empty {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} :
f.support = f = 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

@[instance]
def finsupp.finsupp.decidable_eq {α : Type u_1} {M : Type u_5} [has_zero M] [decidable_eq α] [decidable_eq M] :

Equations
theorem finsupp.finite_supp {α : Type u_1} {M : Type u_5} [has_zero M] (f : α →₀ M) :
{a : α | f a 0}.finite

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

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

Declarations about single

def finsupp.single {α : Type u_1} {M : Type u_5} [has_zero M] :
α → 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} :
(finsupp.single a b) a' = ite (a = a') b 0

@[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} :
a a'(finsupp.single a b) a' = 0

@[simp]
theorem finsupp.single_zero {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} :

theorem finsupp.support_single_ne_zero {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} {b : M} :
b 0(finsupp.single a b).support = {a}

theorem finsupp.support_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 : α) :

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_inj {α : Type u_1} {M : Type u_5} [has_zero M] {a a' : α} {b : M} :
b 0(finsupp.single a b = finsupp.single a' b a = a')

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₁

@[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} :
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

Declarations about on_finset

def finsupp.on_finset {α : Type u_1} {M : Type u_5} [has_zero M] (s : finset α) (f : α → M) :
(∀ (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

Declarations about map_range

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

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

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} :

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

def finsupp.emb_domain {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] :
β)→₀ 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 : β) :

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) :
b 0finsupp.emb_domain f l = finsupp.single a b(∃ (x : α), l = finsupp.single x b f x = a)

Declarations about zip_with

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) :
f 0 0 = 0→₀ M)→₀ 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] {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

def finsupp.erase {α : Type u_1} {M : Type u_5} [has_zero M] :
α → →₀ 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] {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} :
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} :

@[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.sum {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [add_comm_monoid N] :
→₀ M)(α → M → N) → N

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

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

prod f g is the product 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) :
(∀ (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) :
(∀ (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) :
(∀ (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) :
(∀ (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 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 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} :
(∀ (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} :
(∀ (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] (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] (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.prod_ite_eq' {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [comm_monoid N] (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] (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.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) :
(∀ (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) :
(∀ (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.

Additive monoid structure on α →₀ M

@[instance]
def finsupp.has_add {α : Type u_1} {M : Type u_5} [add_monoid M] :

Equations
@[simp]
theorem finsupp.add_apply {α : Type u_1} {M : Type u_5} [add_monoid M] {g₁ g₂ : α →₀ M} {a : α} :
(g₁ + g₂) a = g₁ a + g₂ a

theorem finsupp.support_add {α : Type u_1} {M : Type u_5} [add_monoid M] {g₁ g₂ : α →₀ M} :
(g₁ + g₂).support g₁.support g₂.support

theorem finsupp.support_add_eq {α : Type u_1} {M : Type u_5} [add_monoid M] {g₁ g₂ : α →₀ M} :
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_monoid M] {a : α} {b₁ b₂ : M} :
finsupp.single a (b₁ + b₂) = finsupp.single a b₁ + finsupp.single a b₂

@[instance]
def finsupp.add_monoid {α : Type u_1} {M : Type u_5} [add_monoid M] :

Equations
def finsupp.single_add_hom {α : Type u_1} {M : Type u_5} [add_monoid M] :
α → M →+ α →₀ M

finsupp.single as an add_monoid_hom.

Equations
@[simp]
theorem finsupp.single_add_hom_to_fun {α : Type u_1} {M : Type u_5} [add_monoid M] (a : α) (b : M) :

def finsupp.eval_add_hom {α : Type u_1} {M : Type u_5} [add_monoid M] :
α → →₀ M) →+ M

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

Equations
@[simp]
theorem finsupp.eval_add_hom_apply {α : Type u_1} {M : Type u_5} [add_monoid M] (a : α) (g : α →₀ M) :

theorem finsupp.single_add_erase {α : Type u_1} {M : Type u_5} [add_monoid M] (a : α) (f : α →₀ M) :

theorem finsupp.erase_add_single {α : Type u_1} {M : Type u_5} [add_monoid M] (a : α) (f : α →₀ M) :

@[simp]
theorem finsupp.erase_add {α : Type u_1} {M : Type u_5} [add_monoid M] (a : α) (f f' : α →₀ M) :

theorem finsupp.induction {α : Type u_1} {M : Type u_5} [add_monoid M] {p : →₀ M) → Prop} (f : α →₀ M) :
p 0(∀ (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_monoid M] {p : →₀ M) → Prop} (f : α →₀ M) :
p 0(∀ (a : α) (b : M) (f : α →₀ M), a f.supportb 0p fp (f + finsupp.single a b))p f

@[simp]
theorem finsupp.add_closure_Union_range_single {α : Type u_1} {M : Type u_5} [add_monoid M] :

theorem finsupp.add_hom_ext {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_monoid M] [add_monoid N] ⦃f g : →₀ M) →+ N⦄ :
(∀ (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_monoid M] [add_monoid N] ⦃f g : →₀ M) →+ N⦄ :
(∀ (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_monoid M] [monoid N] ⦃f g : multiplicative →₀ M) →* N⦄ :
(∀ (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_monoid M] [monoid N] {f g : multiplicative →₀ M) →* N} :

theorem finsupp.map_range_add {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_monoid M] [add_monoid 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₂

@[instance]
def finsupp.nat_sub {α : Type u_1} :

Equations
@[simp]
theorem finsupp.nat_sub_apply {α : Type u_1} {g₁ g₂ : α →₀ } {a : α} :
(g₁ - g₂) a = g₁ a - g₂ a

@[simp]
theorem finsupp.single_sub {α : Type u_1} {a : α} {n₁ n₂ : } :
finsupp.single a (n₁ - n₂) = finsupp.single a n₁ - finsupp.single a n₂

theorem finsupp.sub_single_one_add {α : Type u_1} {a : α} {u u' : α →₀ } :
u a 0u - finsupp.single a 1 + u' = u + u' - finsupp.single a 1

theorem finsupp.add_sub_single_one {α : Type u_1} {a : α} {u u' : α →₀ } :
u' a 0u + (u' - finsupp.single a 1) = u + u' - finsupp.single a 1

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} :
(∀ (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} :
(∀ (a : α), h a 0 = 0)(-g).sum h = g.sum (λ (a : α) (b : G), h a (-b))

@[simp]
theorem finsupp.neg_apply {α : Type u_1} {G : Type u_9} [add_group G] {g : α →₀ G} {a : α} :
(-g) a = -g a

@[simp]
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} :

@[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} [has_zero M] [add_comm_monoid N] {f : α →₀ M} {g : α → M → β →₀ N} :
(f.sum g).support f.support.bind (λ (a : α), (g a (f a)).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} :
(∀ (a : α), h a 0 = 0)(∀ (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} :
(∀ (a : α), h a 0 = 1)(∀ (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))

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 : α → β → γ} :
(∀ (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} :
(∀ (a : α), h a 0 = 1)(∀ (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} :
(∀ (a : α), h a 0 = 0)(∀ (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} :
(∀ (a : β), h a 0 = 0)(∀ (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} :
(∀ (a : β), h a 0 = 1)(∀ (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) :
(∀ (a : α), h a 0 = 0)(∀ (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.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)

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] :
(M →+ N)→₀ M) →+ α →₀ N

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

Equations
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)

Declarations about map_domain

def finsupp.map_domain {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] :
(α → β)→₀ 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 : β) :

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 : β → γ} :

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 : α → β} :
(∀ (x : α), x v.supportf x = g x)finsupp.map_domain f v = finsupp.map_domain g v

theorem finsupp.map_domain_add {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] {v₁ v₂ : α →₀ M} {f : α → β} :

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] {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} :
(∀ (a : β), h a 0 = 0)(∀ (a : β) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂)(finsupp.map_domain f s).sum h = s.sum (λ (a : α) (b : M), h (f a) b)

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} :
(∀ (a : β), h a 0 = 1)(∀ (a : β) (b₁ b₂ : M), h a (b₁ + b₂) = (h a b₁) * h a b₂)(finsupp.map_domain f s).prod h = s.prod (λ (a : α) (b : M), h (f a) b)

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} :
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} :
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 : α → β} :

Declarations about comap_domain

def finsupp.comap_domain {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α → β) (l : β →₀ M) :
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) :

Declarations about filter

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

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

Equations
@[simp]
theorem finsupp.filter_apply_pos {α : Type u_1} {M : Type u_5} [has_zero M] (p : α → Prop) (f : α →₀ M) {a : α} :
p a(finsupp.filter p f) a = f a

@[simp]
theorem finsupp.filter_apply_neg {α : Type u_1} {M : Type u_5} [has_zero M] (p : α → Prop) (f : α →₀ M) {a : α} :
¬p a(finsupp.filter p f) a = 0

@[simp]
theorem finsupp.support_filter {α : Type u_1} {M : Type u_5} [has_zero M] (p : α → Prop) (f : α →₀ M) :

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} :

@[simp]
theorem finsupp.filter_single_of_neg {α : Type u_1} {M : Type u_5} [has_zero M] (p : α → Prop) {a : α} {b : M} :

theorem finsupp.filter_pos_add_filter_neg {α : Type u_1} {M : Type u_5} [add_monoid M] (f : α →₀ M) (p : α → Prop) :
finsupp.filter p f + finsupp.filter (λ (a : α), ¬p a) f = f

Declarations about frange

def finsupp.frange {α : Type u_1} {M : Type u_5} [has_zero M] :
→₀ M)finset 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

def finsupp.subtype_domain {α : Type u_1} {M : Type u_5} [has_zero M] (p : α → Prop) :
→₀ M)subtype p →₀ 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} {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} :
(∀ (x : α), x f.supportp x)(finsupp.subtype_domain p f = 0 f = 0)

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} :
(∀ (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} :
(∀ (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_monoid M] {p : α → Prop} {v v' : α →₀ M} :

@[instance]
def finsupp.subtype_domain.is_add_monoid_hom {α : Type u_1} {M : Type u_5} [add_monoid M] {p : α → Prop} :

@[simp]
theorem finsupp.filter_add {α : Type u_1} {M : Type u_5} [add_monoid M] {p : α → Prop} {v v' : α →₀ M} :

@[instance]
def finsupp.filter.is_add_monoid_hom {α : Type u_1} {M : Type u_5} [add_monoid M] (p : α → Prop) :

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)

@[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} :

Declarations relating finsupp to multiset

def finsupp.to_multiset {α : Type u_1} :
→₀ )multiset α

Given f : α →₀ ℕ, f.to_multiset is the multiset with multiplicities given by the values of f on the elements of α.

Equations
@[simp]
theorem finsupp.to_multiset_zero {α : Type u_1} :

@[simp]
theorem finsupp.to_multiset_add {α : Type u_1} (m n : α →₀ ) :

theorem finsupp.to_multiset_single {α : Type u_1} (a : α) (n : ) :

theorem finsupp.card_to_multiset {α : Type u_1} (f : α →₀ ) :
f.to_multiset.card = f.sum (λ (a : α), id)

theorem finsupp.to_multiset_map {α : Type u_1} {β : Type u_2} (f : α →₀ ) (g : α → β) :

theorem finsupp.prod_to_multiset {M : Type u_5} [comm_monoid M] (f : M →₀ ) :
f.to_multiset.prod = f.prod (λ (a : M) (n : ), a ^ n)

theorem finsupp.to_finset_to_multiset {α : Type u_1} (f : α →₀ ) :

@[simp]
theorem finsupp.count_to_multiset {α : Type u_1} (f : α →₀ ) (a : α) :

def finsupp.of_multiset {α : Type u_1} :
multiset αα →₀

Given m : multiset α, of_multiset m is the finitely supported function from α to given by the multiplicities of the elements of α in m.

Equations
@[simp]
theorem finsupp.of_multiset_apply {α : Type u_1} (m : multiset α) (a : α) :

def finsupp.equiv_multiset {α : Type u_1} :

equiv_multiset defines an equiv between finitely supported functions from α to and multisets on α.

Equations
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 : α) :
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

def finsupp.curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] :
× β →₀ 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
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) :
(∀ (a : α) (b : β), g a b 0 = 0)(∀ (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)

def finsupp.uncurry {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] :
→₀ β →₀ 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
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] (f : α × β →₀ M) :

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
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
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
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)

@[instance]
def finsupp.has_scalar {α : Type u_1} {M : Type u_5} {R : Type u_11} [semiring R] [add_comm_monoid M] [semimodule R M] :

Equations
@[simp]
theorem finsupp.smul_apply' (α : Type u_1) (M : Type u_5) {R : Type u_11} {_x : semiring R} [add_comm_monoid M] [semimodule R M] {a : α} {b : R} {v : α →₀ M} :
(b v) a = b v a

@[instance]
def finsupp.semimodule (α : Type u_1) (M : Type u_5) {R : Type u_11} [semiring R] [add_comm_monoid M] [semimodule R M] :

Equations
def finsupp.leval' {α : Type u_1} {M : Type u_5} (R : Type u_11) [semiring R] [add_comm_monoid M] [semimodule R M] :
α → ((α →₀ M) →ₗ[R] M)

Evaluation at point as a linear map. This version assumes that the codomain is a semimodule over some semiring. See also leval.

Equations
@[simp]
theorem finsupp.coe_leval' {α : Type u_1} {M : Type u_5} (R : Type u_11) [semiring R] [add_comm_monoid M] [semimodule R M] (a : α) (g : α →₀ M) :

def finsupp.leval {α : Type u_1} {R : Type u_11} [semiring R] :
α → ((α →₀ R) →ₗ[R] R)

Evaluation at point as a linear map. This version assumes that the codomain is a semiring.

Equations
@[simp]
theorem finsupp.coe_leval {α : Type u_1} {R : Type u_11} [semiring R] (a : α) (g : α →₀ R) :

theorem finsupp.support_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} {_x : semiring R} [add_comm_monoid M] [semimodule 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 : semiring R} [add_comm_monoid M] [semimodule 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 : semiring R} [add_comm_monoid M] [semimodule R M] {f : α → β} (b : R) (v : α →₀ M) :

@[simp]
theorem finsupp.smul_single {α : Type u_1} {M : Type u_5} {R : Type u_11} {_x : semiring R} [add_comm_monoid M] [semimodule 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.smul_single_one {α : Type u_1} {R : Type u_11} [semiring R] (a : α) (b : R) :

@[simp]
theorem finsupp.smul_apply {α : Type u_1} {R : Type u_11} [semiring R] {a : α} {b : R} {v : α →₀ R} :
(b v) a = b v a

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} :
(∀ (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} [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] {g : α →₀ M} {b : R} {h : α → M → N} :
(∀ (i : α), h i 0 = 0)(b g).sum h = g.sum (λ (i : α) (c : M), h i (b c))

theorem finsupp.sum_mul {α : Type u_1} {R : Type u_11} {S : Type u_12} [semiring R] [semiring S] (b : S) (s : α →₀ R) {f : α → R → S} :
(s.sum f) * b = s.sum (λ (a : α) (c : R), (f a c) * b)

theorem finsupp.mul_sum {α : Type u_1} {R : Type u_11} {S : Type u_12} [semiring R] [semiring S] (b : S) (s : α →₀ R) {f : α → R → S} :
b * s.sum f = s.sum (λ (a : α) (c : R), b * f a c)

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

Equations
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
def finsupp.dom_congr {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] :
α β→₀ M) ≃+ →₀ M)

Given add_comm_monoid M and e : α ≃ β, dom_congr e is the corresponding equiv between α →₀ M and β →₀ 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))

Declarations about sigma types

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.

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⟩

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

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 : ι) :

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) :
(∀ (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)

Declarations relating multiset to finsupp

def multiset.to_finsupp {α : Type u_1} :
multiset αα →₀

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} (s : multiset α) :

@[simp]
theorem multiset.to_finsupp_apply {α : Type u_1} (s : multiset α) (a : α) :

@[simp]
theorem multiset.to_finsupp_zero {α : Type u_1} :

@[simp]
theorem multiset.to_finsupp_add {α : Type u_1} (s t : multiset α) :

theorem multiset.to_finsupp_singleton {α : Type u_1} (a : α) :

@[simp]
theorem multiset.to_finsupp_to_multiset {α : Type u_1} (s : multiset α) :

Declarations about order(ed) instances on finsupp

@[instance]
def finsupp.preorder {α : Type u_1} {M : Type u_5} [preorder M] [has_zero M] :

Equations
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

@[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

@[simp]
theorem finsupp.to_multiset_to_finsupp {α : Type u_1} (f : α →₀ ) :

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

theorem finsupp.lt_wf (α : Type u_1) :

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

@[instance]

Equations
def finsupp.antidiagonal {α : Type u_1} :
→₀ )→₀ ) × →₀ ) →₀

The finsupp counterpart of multiset.antidiagonal: the antidiagonal of s : α →₀ ℕ consists of all pairs (t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ) such that t₁ + t₂ = s. The finitely supported function antidiagonal s is equal to the multiplicities of these pairs.

Equations
theorem finsupp.mem_antidiagonal_support {α : Type u_1} {f : α →₀ } {p : →₀ ) × →₀ )} :

@[simp]
theorem finsupp.antidiagonal_zero {α : Type u_1} :

theorem finsupp.swap_mem_antidiagonal_support {α : Type u_1} {n : α →₀ } {f : →₀ ) × →₀ )} :

theorem finsupp.finite_le_nat {α : Type u_1} (n : α →₀ ) :
{m : α →₀ | m n}.finite

Let n : α →₀ ℕ be a finitely supported function. The set of m : α →₀ ℕ that are coordinatewise less than or equal to n, is a finite set.

theorem finsupp.finite_lt_nat {α : Type u_1} (n : α →₀ ) :
{m : α →₀ | m < n}.finite

Let n : α →₀ ℕ be a finitely supported function. The set of m : α →₀ ℕ that are coordinatewise less than or equal to n, but not equal to n everywhere, is a finite set.