# mathlib3documentation

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:

• `monoid_algebra R M` and `add_monoid_algebra R M` are defined as `M →₀ R`;

• polynomials and multivariate polynomials are defined as `add_monoid_algebra`s, hence they use `finsupp` under the hood;

• the linear combination of a family of vectors `v i` with coefficients `f i` (as used, e.g., to define linearly independent family `linear_independent`) is defined as a map `finsupp.total : (ι → M) → (ι →₀ R) →ₗ[R] M`.

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

• `multiset α ≃+ α →₀ ℕ`;
• `free_abelian_group α ≃+ α →₀ ℤ`.

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 #

• `finsupp`: The type of finitely supported functions from `α` to `β`.
• `finsupp.single`: The `finsupp` which is nonzero in exactly one point.
• `finsupp.update`: Changes one value of a `finsupp`.
• `finsupp.erase`: Replaces one value of a `finsupp` by `0`.
• `finsupp.on_finset`: The restriction of a function to a `finset` as a `finsupp`.
• `finsupp.map_range`: Composition of a `zero_hom` with a `finsupp`.
• `finsupp.emb_domain`: Maps the domain of a `finsupp` by an embedding.
• `finsupp.zip_with`: Postcomposition of two `finsupp`s with a function `f` such that `f 0 0 = 0`.

## Notations #

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

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

• `α`, `β`, `γ`: types with no additional structure that appear as the first argument to `finsupp` somewhere in the statement;

• `ι` : an auxiliary index type;

• `M`, `M'`, `N`, `P`: types with `has_zero` or `(add_)(comm_)monoid` structure; `M` is also used for a (semi)module over a (semi)ring.

• `G`, `H`: groups (commutative or not, multiplicative or additive);

• `R`, `S`: (semi)rings.

## Implementation notes #

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

## TODO #

• Expand the list of definitions and important lemmas to the module docstring.
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`.

Instances for `finsupp`

### 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 = 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) (ᾰ : α) :
= f ᾰ
@[simp]
theorem finsupp.equiv_fun_on_finite_symm_apply_support {α : 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_symm_apply_support_val {M : Type u_5} [has_zero M] {ι : Type u_1} [unique ι] (ᾰ : M) :
@[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}  :
f = g
theorem finsupp.unique_ext_iff {α : Type u_1} {M : Type u_5} [has_zero M] [unique α] {f g : α →₀ M} :
f = g

### 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')] :
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) = y) z
theorem finsupp.single_eq_set_indicator {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} {b : M} :
b) = {a}.indicator (λ (_x : α), b)
@[simp]
theorem finsupp.single_eq_same {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} {b : M} :
b) a = b
@[simp]
theorem finsupp.single_eq_of_ne {α : Type u_1} {M : Type u_5} [has_zero M] {a a' : α} {b : M} (h : a a') :
b) a' = 0
theorem finsupp.single_eq_update {α : Type u_1} {M : Type u_5} [has_zero M] [decidable_eq α] (a : α) (b : M) :
b) = b
theorem finsupp.single_eq_pi_single {α : Type u_1} {M : Type u_5} [has_zero M] [decidable_eq α] (a : α) (b : M) :
b) = b
@[simp]
theorem finsupp.single_zero {α : Type u_1} {M : Type u_5} [has_zero M] (a : α) :
= 0
theorem finsupp.single_of_single_apply {α : Type u_1} {M : Type u_5} [has_zero M] (a a' : α) (b : M) :
( b) a) = b)) a
theorem finsupp.support_single_ne_zero {α : Type u_1} {M : Type u_5} [has_zero M] {b : M} (a : α) (hb : b 0) :
b).support = {a}
theorem finsupp.support_single_subset {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} {b : M} :
b).support {a}
theorem finsupp.single_apply_mem {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} {b : M} (x : α) :
b) x {0, b}
theorem finsupp.range_single_subset {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} {b : M} :
set.range b) {0, b}
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} :
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} :
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 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 = 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) :
b₁ = 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) :
function.injective (λ (a : α), b)

`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) :
= b a = a'
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 : α} :
b').support i j
@[simp]
theorem finsupp.single_eq_zero {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} {b : M} :
= 0 b = 0
theorem finsupp.single_swap {α : Type u_1} {M : Type u_5} [has_zero M] (a₁ a₂ : α) (b : M) :
b) 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) :
@[simp]
theorem finsupp.unique_single_eq_iff {α : Type u_1} {M : Type u_5} [has_zero M] {a a' : α} {b : M} [unique α] {b' : M} :
= b' b = b'
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 = (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 =
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 = (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 =
theorem finsupp.support_subset_singleton {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} {a : α} :
f.support {a} f = (f 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 =
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 = (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 =
@[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]
theorem finsupp.equiv_fun_on_finite_symm_single {α : Type u_1} {M : Type u_5} [has_zero M] [decidable_eq α] [finite α] (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 α] :
(f.update a b) = b
@[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) :
0.update a b =
theorem finsupp.support_update {α : Type u_1} {M : Type u_5} [has_zero M] (f : α →₀ M) (a : α) (b : M) [decidable_eq α] [decidable_eq M] :
(f.update a b).support = ite (b = 0) (f.support.erase 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) :
(f.update a b).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`. 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} :
f) a = 0
@[simp]
theorem finsupp.erase_ne {α : Type u_1} {M : Type u_5} [has_zero M] {a a' : α} {f : α →₀ M} (h : a' a) :
f) a' = f a'
@[simp]
theorem finsupp.erase_single {α : Type u_1} {M : Type u_5} [has_zero M] {a : α} {b : M} :
b) = 0
theorem finsupp.erase_single_ne {α : Type u_1} {M : Type u_5} [has_zero M] {a a' : α} {b : M} (h : a a') :
b) = b
@[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) :
= f
@[simp]
theorem finsupp.erase_zero {α : Type u_1} {M : Type u_5} [has_zero M] (a : α) :
= 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 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 : α} :
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} :
hf).support 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 : α} :
a hf).support f a 0
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) :
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 : .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 : .finite} :
= f
@[protected, instance]
def finsupp.can_lift {α : Type u_1} {M : Type u_5} [has_zero M] :
can_lift M) →₀ M) coe_fn (λ (f : α M), .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`):

• `finsupp.map_range.equiv`
• `finsupp.map_range.zero_hom`
• `finsupp.map_range.add_monoid_hom`
• `finsupp.map_range.add_equiv`
• `finsupp.map_range.linear_map`
• `finsupp.map_range.linear_equiv`
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 : α} :
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} :
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 = 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} :
b) = (f b)
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) :
he0 f).support = f.support

### 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) :
v).support =
@[simp]
theorem finsupp.emb_domain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) :
= 0
@[simp]
theorem finsupp.emb_domain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (v : α →₀ M) (a : α) :
v) (f a) = v 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 ) :
v) a = 0
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} :
= 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} :
= 0 l = 0
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) :
hg p) = p)
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 : = ) :
(x : α), l = 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) :
m) = finsupp.single (f a) 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 : α} :
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} :
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}  :
Equations
@[simp]
theorem finsupp.coe_add {α : Type u_1} {M : Type u_5} (f g : α →₀ M) :
(f + g) = f + g
theorem finsupp.add_apply {α : Type u_1} {M : Type u_5} (g₁ g₂ : α →₀ M) (a : α) :
(g₁ + g₂) a = g₁ a + g₂ a
theorem finsupp.support_add {α : Type u_1} {M : Type u_5} [decidable_eq α] {g₁ g₂ : α →₀ M} :
(g₁ + g₂).support g₁.support g₂.support
theorem finsupp.support_add_eq {α : Type u_1} {M : Type u_5} [decidable_eq α] {g₁ g₂ : α →₀ M} (h : g₂.support) :
(g₁ + g₂).support = g₁.support g₂.support
@[simp]
theorem finsupp.single_add {α : Type u_1} {M : Type u_5} (a : α) (b₁ b₂ : M) :
(b₁ + b₂) = b₁ + b₂
@[protected, instance]
noncomputable def finsupp.add_zero_class {α : Type u_1} {M : Type u_5}  :
Equations
noncomputable def finsupp.single_add_hom {α : Type u_1} {M : Type u_5} (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} (a : α) (b : M) :
=
def finsupp.apply_add_hom {α : Type u_1} {M : Type u_5} (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} (a : α) (g : α →₀ M) :
= g a
@[simp]
theorem finsupp.coe_fn_add_hom_apply {α : Type u_1} {M : Type u_5} (x : α →₀ M) (ᾰ : α) :
= x ᾰ
def finsupp.coe_fn_add_hom {α : Type u_1} {M : Type u_5}  :
→₀ 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} (f : α →₀ M) (a : α) (b : M) :
f.update a b = +
theorem finsupp.update_eq_erase_add_single {α : Type u_1} {M : Type u_5} (f : α →₀ M) (a : α) (b : M) :
f.update a b = +
theorem finsupp.single_add_erase {α : Type u_1} {M : Type u_5} (a : α) (f : α →₀ M) :
(f a) + = f
theorem finsupp.erase_add_single {α : Type u_1} {M : Type u_5} (a : α) (f : α →₀ M) :
+ (f a) = f
@[simp]
theorem finsupp.erase_add {α : Type u_1} {M : Type u_5} (a : α) (f f' : α →₀ M) :
(f + f') = + f'
@[simp]
theorem finsupp.erase_add_hom_apply {α : Type u_1} {M : Type u_5} (a : α) (f : α →₀ M) :
=
noncomputable def finsupp.erase_add_hom {α : Type u_1} {M : Type u_5} (a : α) :
→₀ M) →+ α →₀ M

`finsupp.erase` as an `add_monoid_hom`.

Equations
@[protected]
theorem finsupp.induction {α : Type u_1} {M : Type u_5} {p : →₀ M) Prop} (f : α →₀ M) (h0 : p 0) (ha : (a : α) (b : M) (f : α →₀ M), a f.support b 0 p f p b + f)) :
p f
theorem finsupp.induction₂ {α : Type u_1} {M : Type u_5} {p : →₀ M) Prop} (f : α →₀ M) (h0 : p 0) (ha : (a : α) (b : M) (f : α →₀ M), a f.support b 0 p f p (f + b)) :
p f
theorem finsupp.induction_linear {α : Type u_1} {M : Type u_5} {p : →₀ M) Prop} (f : α →₀ M) (h0 : p 0) (hadd : (f g : α →₀ M), p f p g p (f + g)) (hsingle : (a : α) (b : M), p b)) :
p f
@[simp]
theorem finsupp.add_closure_set_of_eq_single {α : Type u_1} {M : Type u_5}  :
add_submonoid.closure {f : α →₀ M | (a : α) (b : M), f = b} =
theorem finsupp.add_hom_ext {α : Type u_1} {M : Type u_5} {N : Type u_7} ⦃f g : →₀ M) →+ N⦄ (H : (x : α) (y : M), f y) = g 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} ⦃f g : →₀ M) →+ N⦄ (H : (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_hom`s 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} ⦃f g : multiplicative →₀ M) →* N⦄ (H : (x : α) (y : M), f = g ) :
f = g
@[ext]
theorem finsupp.mul_hom_ext' {α : Type u_1} {M : Type u_5} {N : Type u_7} {f g : multiplicative →₀ M) →* N} (H : (x : α), ) :
f = g
theorem finsupp.map_range_add {α : Type u_1} {M : Type u_5} {N : Type u_7} {f : M N} {hf : f 0 = 0} (hf' : (x y : M), f (x + y) = f x + f y) (v₁ v₂ : α →₀ M) :
(v₁ + v₂) = v₁ + v₂
theorem finsupp.map_range_add' {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [ N] {f : β} (v₁ v₂ : α →₀ M) :
(v₁ + v₂) = v₁ + v₂
@[simp]
theorem finsupp.emb_domain.add_monoid_hom_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} (f : α β) (v : α →₀ M) :
noncomputable def finsupp.emb_domain.add_monoid_hom {α : Type u_1} {β : Type u_2} {M : Type u_5} (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} (f : α β) (v w : α →₀ M) :
(v + w) =
@[protected, instance]
noncomputable def finsupp.has_nat_scalar {α : Type u_1} {M : Type u_5} [add_monoid M] :
→₀ 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}  :
Equations
@[protected, instance]
noncomputable def finsupp.has_neg {α : Type u_1} {G : Type u_9}  :
Equations
@[simp]
theorem finsupp.coe_neg {α : Type u_1} {G : Type u_9} (g : α →₀ G) :
theorem finsupp.neg_apply {α : Type u_1} {G : Type u_9} (g : α →₀ G) (a : α) :
(-g) a = -g a
theorem finsupp.map_range_neg {α : Type u_1} {G : Type u_9} {H : Type u_10} {f : G H} {hf : f 0 = 0} (hf' : (x : G), f (-x) = -f x) (v : α →₀ G) :
(-v) = - v
theorem finsupp.map_range_neg' {α : Type u_1} {β : Type u_2} {G : Type u_9} {H : Type u_10} [add_group G] [ H] {f : β} (v : α →₀ G) :
(-v) = - v
@[protected, instance]
noncomputable def finsupp.has_sub {α : Type u_1} {G : Type u_9}  :
Equations
@[simp]
theorem finsupp.coe_sub {α : Type u_1} {G : Type u_9} (g₁ g₂ : α →₀ G) :
(g₁ - g₂) = g₁ - g₂
theorem finsupp.sub_apply {α : Type u_1} {G : Type u_9} (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} {f : G H} {hf : f 0 = 0} (hf' : (x y : G), f (x - y) = f x - f y) (v₁ v₂ : α →₀ G) :
(v₁ - v₂) = v₁ - v₂
theorem finsupp.map_range_sub' {α : Type u_1} {β : Type u_2} {G : Type u_9} {H : Type u_10} [add_group G] [ H] {f : β} (v₁ v₂ : α →₀ G) :
(v₁ - v₂) = v₁ - v₂
@[protected, instance]
noncomputable def finsupp.has_int_scalar {α : Type u_1} {G : Type u_9} [add_group G] :
→₀ 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