mathlib3 documentation

data.finsupp.defs

Type of functions with finite support #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

For any type α and any 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, which is defined in algebra/big_operators/finsupp.

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.

Main declarations #

Notations #

This file adds α →₀ M as a global notation for finsupp α M.

We also use the following convention for Type* variables in this file

Implementation notes #

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

TODO #

Basic declarations about finsupp #

@[protected, instance]
def finsupp.fun_like {α : Type u_1} {M : Type u_5} [has_zero M] :
fun_like →₀ M) α (λ (_x : α), M)
Equations
@[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)

Helper instance for when there are too many metavariables to apply fun_like.has_coe_to_fun directly.

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

Deprecated. Use fun_like.ext_iff instead.

theorem finsupp.coe_fn_inj {α : Type u_1} {M : Type u_5} [has_zero M] {f g : α →₀ M} :
f = g f = g

Deprecated. Use fun_like.coe_fn_eq instead.

theorem finsupp.coe_fn_injective {α : Type u_1} {M : Type u_5} [has_zero M] :

Deprecated. Use fun_like.coe_injective instead.

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

Deprecated. Use fun_like.congr_fun instead.

@[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
@[simp, norm_cast]
theorem finsupp.coe_eq_zero {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} :
f = 0 f = 0
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.support f 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.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 s f a = 0
@[simp]
theorem finsupp.equiv_fun_on_finite_symm_apply_to_fun {α : Type u_1} {M : Type u_5} [has_zero M] [finite α] (f : α M) (ᾰ : α) :
noncomputable def finsupp.equiv_fun_on_finite {α : Type u_1} {M : Type u_5} [has_zero M] [finite α] :
→₀ M) M)

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

Equations
@[simp]
theorem finsupp.equiv_fun_on_finite_apply {α : Type u_1} {M : Type u_5} [has_zero M] [finite α] (x : α →₀ M) (ᾰ : α) :
@[simp]
theorem finsupp.equiv_fun_on_finite_symm_coe {M : Type u_5} [has_zero M] {α : Type u_1} [finite α] (f : α →₀ M) :
@[simp]
theorem equiv.finsupp_unique_symm_apply_to_fun {M : Type u_5} [has_zero M] {ι : Type u_1} [unique ι] (ᾰ : M) (ᾰ_1 : ι) :
noncomputable def equiv.finsupp_unique {M : Type u_5} [has_zero M] {ι : Type u_1} [unique ι] :
→₀ M) M

If α has a unique term, the type of finitely supported functions α →₀ β is equivalent to β.

Equations
@[simp]
theorem equiv.finsupp_unique_apply {M : Type u_5} [has_zero M] {ι : Type u_1} [unique ι] (ᾰ : ι →₀ M) :
@[ext]
theorem finsupp.unique_ext {α : Type u_1} {M : Type u_5} [has_zero M] [unique α] {f g : α →₀ M} (h : f inhabited.default = g inhabited.default) :
f = g
theorem finsupp.unique_ext_iff {α : Type u_1} {M : Type u_5} [has_zero M] [unique α] {f g : α →₀ 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 with 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_apply_left {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] {f : α β} (hf : function.injective f) (x z : α) (y : M) :
(finsupp.single (f x) y) (f z) = (finsupp.single x y) z
theorem finsupp.single_eq_set_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] [decidable_eq α] (a : α) (b : M) :
theorem finsupp.single_eq_pi_single {α : Type u_1} {M : Type u_5} [has_zero M] [decidable_eq α] (a : α) (b : M) :
@[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] {b : M} (a : α) (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 = a b = 0
theorem finsupp.single_apply_ne_zero {α : Type u_1} {M : Type u_5} [has_zero M] {a x : α} {b : M} :
(finsupp.single a b) x 0 x = a b 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 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] :
@[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_finite_single {α : Type u_1} {M : Type u_5} [has_zero M] [decidable_eq α] [finite α] (x : α) (m : M) :
@[simp]

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
@[simp]
theorem finsupp.zero_update {α : Type u_1} {M : Type u_5} [has_zero M] (a : α) (b : M) :
theorem finsupp.support_update {α : Type u_1} {M : Type u_5} [has_zero M] (f : α →₀ M) (a : α) (b : M) [decidable_eq α] [decidable_eq M] :
@[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 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. If a is not in the support of f then erase a f = f.

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 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 0 a s) :
α →₀ M

on_finset s f hf is the finsupp function representing f restricted to the finset s. The function must 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 0 a 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 0 a 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 0 a s) {a : α} :
theorem finsupp.support_on_finset {α : Type u_1} {M : Type u_5} [has_zero M] [decidable_eq M] {s : finset α} {f : α M} (hf : (a : α), f a 0 a 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) coe_fn (λ (f : α M), (function.support f).finite)
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, which is well-defined when f 0 = 0.

This preserves the structure on f, and exists in various bundled forms for when f is itself bundled (defined in data/finsupp/basic):

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} :
theorem finsupp.support_map_range_of_injective {ι : Type u_4} {M : Type u_5} {N : Type u_7} [has_zero M] [has_zero N] {e : M N} (he0 : e 0 = 0) (f : ι →₀ M) (he : function.injective e) :

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

Given finitely supported functions g₁ : α →₀ M and g₂ : α →₀ N and function f : M → N → P, zip_with f hf g₁ g₂ is the finitely supported function α →₀ P satisfying zip_with f hf g₁ g₂ a = f (g₁ a) (g₂ a), which 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

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 in linear_algebra/finsupp 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) :
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 in linear_algebra/finsupp 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) :
@[simp]
theorem finsupp.coe_fn_add_hom_apply {α : Type u_1} {M : Type u_5} [add_zero_class M] (x : α →₀ M) (ᾰ : α) :
def finsupp.coe_fn_add_hom {α : Type u_1} {M : Type u_5} [add_zero_class M] :
→₀ M) →+ α M

Coercion from a finsupp to a function type is an add_monoid_hom.

Equations
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.support b 0 p f p (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.support b 0 p f p (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 f p g p (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
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₂
theorem finsupp.map_range_add' {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [add_zero_class M] [add_zero_class N] [add_monoid_hom_class β M N] {f : β} (v₁ v₂ : α →₀ M) :
@[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.has_nat_scalar {α : Type u_1} {M : Type u_5} [add_monoid M] :

Note the general finsupp.has_smul instance doesn't apply as is not distributive unless β i's addition is commutative.

Equations
@[protected, instance]
noncomputable def finsupp.add_monoid {α : Type u_1} {M : Type u_5} [add_monoid M] :
Equations
@[protected, instance]
noncomputable def finsupp.add_comm_monoid {α : Type u_1} {M : Type u_5} [add_comm_monoid M] :
Equations
@[protected, instance]
noncomputable def finsupp.has_neg {α : Type u_1} {G : Type u_9} [neg_zero_class G] :
Equations
@[simp]
theorem finsupp.coe_neg {α : Type u_1} {G : Type u_9} [neg_zero_class G] (g : α →₀ G) :
theorem finsupp.neg_apply {α : Type u_1} {G : Type u_9} [neg_zero_class G] (g : α →₀ G) (a : α) :
(-g) a = -g a
theorem finsupp.map_range_neg {α : Type u_1} {G : Type u_9} {H : Type u_10} [neg_zero_class G] [neg_zero_class H] {f : G H} {hf : f 0 = 0} (hf' : (x : G), f (-x) = -f x) (v : α →₀ G) :
theorem finsupp.map_range_neg' {α : Type u_1} {β : Type u_2} {G : Type u_9} {H : Type u_10} [add_group G] [subtraction_monoid H] [add_monoid_hom_class β G H] {f : β} (v : α →₀ G) :
@[protected, instance]
noncomputable def finsupp.has_sub {α : Type u_1} {G : Type u_9} [sub_neg_zero_monoid G] :
Equations
@[simp]
theorem finsupp.coe_sub {α : Type u_1} {G : Type u_9} [sub_neg_zero_monoid G] (g₁ g₂ : α →₀ G) :
(g₁ - g₂) = g₁ - g₂
theorem finsupp.sub_apply {α : Type u_1} {G : Type u_9} [sub_neg_zero_monoid G] (g₁ g₂ : α →₀ G) (a : α) :
(g₁ - g₂) a = g₁ a - g₂ a
theorem finsupp.map_range_sub {α : Type u_1} {G : Type u_9} {H : Type u_10} [sub_neg_zero_monoid G] [sub_neg_zero_monoid H] {f : G H} {hf : f 0 = 0} (hf' : (x y : G), f (x - y) = f x - f y) (v₁ v₂ : α →₀ G) :
finsupp.map_range f hf (v₁ - v₂) = finsupp.map_range f hf v₁ - finsupp.map_range f hf v₂
theorem finsupp.map_range_sub' {α : Type u_1} {β : Type u_2} {G : Type u_9} {H : Type u_10} [add_group G] [subtraction_monoid H] [add_monoid_hom_class β G H] {f : β} (v₁ v₂ : α →₀ G) :
@[protected, instance]
noncomputable def finsupp.has_int_scalar {α : Type u_1} {G : Type u_9} [add_group G] :

Note the general finsupp.has_smul instance doesn't apply as is not distributive unless β i's addition is commutative.

Equations
@[protected, instance]
noncomputable def finsupp.add_group {α : Type u_1} {G : Type u_9} [add_group G] :
Equations
@[protected, instance]
noncomputable def finsupp.add_comm_group {α : Type u_1} {G : Type u_9} [add_comm_group G] :
Equations
theorem finsupp.single_add_single_eq_single_add_single {α : Type u_1} {M : Type u_5} [add_comm_monoid M] {k l m n : α} {u v : M} (hu : u 0) (hv : v 0) :
finsupp.single k u + finsupp.single l v = finsupp.single m u + finsupp.single n v k = m l = n u = v k = n l = m u + v = 0 k = l m = n
@[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) :