# Type of functions with finite support #

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:

• MonoidAlgebra R M and AddMonoidAlgebra R M are defined as M →₀ R;

• polynomials and multivariate polynomials are defined as AddMonoidAlgebras, 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 LinearIndependent) is defined as a map Finsupp.linearCombination : (ι → 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 α ≃+ α →₀ ℕ;
• FreeAbelianGroup α ≃+ α →₀ ℤ.

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/BigOperators/Finsupp.

-- Porting note: the semireducibility remark no longer applies in Lean 4, afaict. Many constructions based on α →₀ M use semireducible type tags to avoid reusing unwanted type instances. E.g., MonoidAlgebra, AddMonoidAlgebra, 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.onFinset: The restriction of a function to a Finset as a Finsupp.
• Finsupp.mapRange: Composition of a ZeroHom with a Finsupp.
• Finsupp.embDomain: Maps the domain of a Finsupp by an embedding.
• Finsupp.zipWith: Postcomposition of two Finsupps 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 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) [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.

• support :

The support of a finitely supported function (aka Finsupp).

• toFun : αM

The underlying function of a bundled finitely supported function (aka Finsupp).

• mem_support_toFun : ∀ (a : α), a self.support self.toFun a 0

The witness that the support of a Finsupp is indeed the exact locus where its underlying function is nonzero.

Instances For
theorem Finsupp.mem_support_toFun {α : Type u_13} {M : Type u_14} [Zero M] (self : α →₀ M) (a : α) :
a self.support self.toFun a 0

The witness that the support of a Finsupp is indeed the exact locus where its underlying function is nonzero.

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

Equations
Instances For

### Basic declarations about Finsupp#

instance Finsupp.instFunLike {α : Type u_1} {M : Type u_5} [Zero M] :
FunLike (α →₀ M) α M
Equations
• Finsupp.instFunLike = { coe := Finsupp.toFun, coe_injective' := }
instance Finsupp.instCoeFun {α : Type u_1} {M : Type u_5} [Zero M] :
CoeFun (α →₀ M) fun (x : α →₀ M) => αM

Helper instance for when there are too many metavariables to apply the DFunLike instance directly.

Equations
• Finsupp.instCoeFun = inferInstance
theorem Finsupp.ext_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {g : α →₀ M} :
f = g ∀ (a : α), f a = g a
theorem Finsupp.ext {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {g : α →₀ M} (h : ∀ (a : α), f a = g a) :
f = g
theorem Finsupp.ne_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {g : α →₀ M} :
f g ∃ (a : α), f a g a
@[simp]
theorem Finsupp.coe_mk {α : Type u_1} {M : Type u_5} [Zero M] (f : αM) (s : ) (h : ∀ (a : α), a s f a 0) :
{ support := s, toFun := f, mem_support_toFun := h } = f
instance Finsupp.instZero {α : Type u_1} {M : Type u_5} [Zero M] :
Zero (α →₀ M)
Equations
• Finsupp.instZero = { zero := { support := , toFun := 0, mem_support_toFun := } }
@[simp]
theorem Finsupp.coe_zero {α : Type u_1} {M : Type u_5} [Zero M] :
0 = 0
theorem Finsupp.zero_apply {α : Type u_1} {M : Type u_5} [Zero M] {a : α} :
0 a = 0
@[simp]
theorem Finsupp.support_zero {α : Type u_1} {M : Type u_5} [Zero M] :
instance Finsupp.instInhabited {α : Type u_1} {M : Type u_5} [Zero M] :
Equations
• Finsupp.instInhabited = { default := 0 }
@[simp]
theorem Finsupp.mem_support_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} :
a f.support f a 0
@[simp]
theorem Finsupp.fun_support_eq {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) :
= f.support
theorem Finsupp.not_mem_support_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} :
af.support f a = 0
@[simp]
theorem Finsupp.coe_eq_zero {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
f = 0 f = 0
theorem Finsupp.ext_iff' {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {g : α →₀ M} :
f = g f.support = g.support xf.support, f x = g x
@[simp]
theorem Finsupp.support_eq_empty {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
f.support = f = 0
theorem Finsupp.support_nonempty_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
f.support.Nonempty f 0
theorem Finsupp.card_support_eq_zero {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
f.support.card = 0 f = 0
instance Finsupp.instDecidableEq {α : Type u_1} {M : Type u_5} [Zero M] [] [] :
Equations
theorem Finsupp.finite_support {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) :
(Function.support f).Finite
theorem Finsupp.support_subset_iff {α : Type u_1} {M : Type u_5} [Zero M] {s : Set α} {f : α →₀ M} :
f.support s as, f a = 0
@[simp]
theorem Finsupp.equivFunOnFinite_symm_apply_support {α : Type u_1} {M : Type u_5} [Zero M] [] (f : αM) :
(Finsupp.equivFunOnFinite.symm f).support = .toFinset
@[simp]
theorem Finsupp.equivFunOnFinite_symm_apply_toFun {α : Type u_1} {M : Type u_5} [Zero M] [] (f : αM) :
∀ (a : α), (Finsupp.equivFunOnFinite.symm f) a = f a
@[simp]
theorem Finsupp.equivFunOnFinite_apply {α : Type u_1} {M : Type u_5} [Zero M] [] :
∀ (a : α →₀ M) (a_1 : α), Finsupp.equivFunOnFinite a a_1 = a a_1
def Finsupp.equivFunOnFinite {α : Type u_1} {M : Type u_5} [Zero M] [] :
(α →₀ M) (αM)

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

Equations
• Finsupp.equivFunOnFinite = { toFun := DFunLike.coe, invFun := fun (f : αM) => { support := .toFinset, toFun := f, mem_support_toFun := }, left_inv := , right_inv := }
Instances For
@[simp]
theorem Finsupp.equivFunOnFinite_symm_coe {M : Type u_5} [Zero M] {α : Type u_13} [] (f : α →₀ M) :
Finsupp.equivFunOnFinite.symm f = f
@[simp]
theorem Equiv.finsuppUnique_apply {M : Type u_5} [Zero M] {ι : Type u_13} [] :
∀ (a : ι →₀ M), Equiv.finsuppUnique a = a default
@[simp]
theorem Equiv.finsuppUnique_symm_apply_support_val {M : Type u_5} [Zero M] {ι : Type u_13} [] :
∀ (a : M), (Equiv.finsuppUnique.symm a).support.val = Multiset.map Subtype.val Finset.univ.val
@[simp]
theorem Equiv.finsuppUnique_symm_apply_toFun {M : Type u_5} [Zero M] {ι : Type u_13} [] :
∀ (a : M) (a_1 : ι), (Equiv.finsuppUnique.symm a) a_1 = a
noncomputable def Equiv.finsuppUnique {M : Type u_5} [Zero M] {ι : Type u_13} [] :
(ι →₀ M) M

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

Equations
Instances For
theorem Finsupp.unique_ext_iff {α : Type u_1} {M : Type u_5} [Zero M] [] {f : α →₀ M} {g : α →₀ M} :
f = g f default = g default
theorem Finsupp.unique_ext {α : Type u_1} {M : Type u_5} [Zero M] [] {f : α →₀ M} {g : α →₀ M} (h : f default = g default) :
f = g

### Declarations about single#

def Finsupp.single {α : Type u_1} {M : Type u_5} [Zero M] (a : α) (b : M) :
α →₀ M

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

Equations
• = { support := if b = 0 then else {a}, toFun := , mem_support_toFun := }
Instances For
theorem Finsupp.single_apply {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {a' : α} {b : M} [Decidable (a = a')] :
(Finsupp.single a b) a' = if a = a' then b else 0
theorem Finsupp.single_apply_left {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : αβ} (hf : ) (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} [Zero M] {a : α} {b : M} :
(Finsupp.single a b) = {a}.indicator fun (x : α) => b
@[simp]
theorem Finsupp.single_eq_same {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} :
(Finsupp.single a b) a = b
@[simp]
theorem Finsupp.single_eq_of_ne {α : Type u_1} {M : Type u_5} [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} [Zero M] [] (a : α) (b : M) :
(Finsupp.single a b) =
theorem Finsupp.single_eq_pi_single {α : Type u_1} {M : Type u_5} [Zero M] [] (a : α) (b : M) :
(Finsupp.single a b) =
@[simp]
theorem Finsupp.single_zero {α : Type u_1} {M : Type u_5} [Zero M] (a : α) :
= 0
theorem Finsupp.single_of_single_apply {α : Type u_1} {M : Type u_5} [Zero M] (a : α) (a' : α) (b : M) :
theorem Finsupp.support_single_ne_zero {α : Type u_1} {M : Type u_5} [Zero M] {b : M} (a : α) (hb : b 0) :
(Finsupp.single a b).support = {a}
theorem Finsupp.support_single_subset {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} :
(Finsupp.single a b).support {a}
theorem Finsupp.single_apply_mem {α : Type u_1} {M : Type u_5} [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} [Zero M] {a : α} {b : M} :
Set.range (Finsupp.single a b) {0, b}
theorem Finsupp.single_injective {α : Type u_1} {M : Type u_5} [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} [Zero M] {a : α} {x : α} {b : M} :
(Finsupp.single a b) x = 0 x = ab = 0
theorem Finsupp.single_apply_ne_zero {α : Type u_1} {M : Type u_5} [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} [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} [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} [Zero M] (a₁ : α) (a₂ : α) (b₁ : M) (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} [Zero M] {b : M} (h : b 0) :
Function.Injective fun (a : α) =>

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} [Zero M] {a : α} {a' : α} {b : M} (h : b 0) :
= a = a'
theorem Finsupp.support_single_ne_bot {α : Type u_1} {M : Type u_5} [Zero M] {b : M} (i : α) (h : b 0) :
(Finsupp.single i b).support
theorem Finsupp.support_single_disjoint {α : Type u_1} {M : Type u_5} [Zero M] {b : M} {b' : M} (hb : b 0) (hb' : b' 0) {i : α} {j : α} :
Disjoint (Finsupp.single i b).support (Finsupp.single j b').support i j
@[simp]
theorem Finsupp.single_eq_zero {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} :
= 0 b = 0
theorem Finsupp.single_swap {α : Type u_1} {M : Type u_5} [Zero M] (a₁ : α) (a₂ : α) (b : M) :
(Finsupp.single a₁ b) a₂ = (Finsupp.single a₂ b) a₁
instance Finsupp.instNontrivial {α : Type u_1} {M : Type u_5} [Zero M] [] [] :
Equations
• =
theorem Finsupp.unique_single {α : Type u_1} {M : Type u_5} [Zero M] [] (x : α →₀ M) :
x = Finsupp.single default (x default)
@[simp]
theorem Finsupp.unique_single_eq_iff {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {a' : α} {b : M} [] {b' : M} :
= Finsupp.single a' b' b = b'
theorem Finsupp.apply_single' {α : Type u_1} {N : Type u_7} {P : Type u_8} [Zero N] [Zero P] (e : NP) (he : e 0 = 0) (a : α) (n : N) (b : α) :
e ((Finsupp.single a n) b) = (Finsupp.single a (e n)) b
theorem Finsupp.apply_single {α : Type u_1} {N : Type u_7} {P : Type u_8} [Zero N] [Zero P] {F : Type u_13} [FunLike F N P] [ZeroHomClass F N P] (e : F) (a : α) (n : N) (b : α) :
e ((Finsupp.single a n) b) = (Finsupp.single a (e n)) b
theorem Finsupp.support_eq_singleton {α : Type u_1} {M : Type u_5} [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} [Zero M] {f : α →₀ M} {a : α} :
f.support = {a} ∃ (b : M), b 0 f =
theorem Finsupp.card_support_eq_one {α : Type u_1} {M : Type u_5} [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} [Zero M] {f : α →₀ M} :
f.support.card = 1 ∃ (a : α) (b : M), b 0 f =
theorem Finsupp.support_subset_singleton {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} :
f.support {a} f = Finsupp.single a (f a)
theorem Finsupp.support_subset_singleton' {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} :
f.support {a} ∃ (b : M), f =
theorem Finsupp.card_support_le_one {α : Type u_1} {M : Type u_5} [Zero M] [] {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} [Zero M] [] {f : α →₀ M} :
f.support.card 1 ∃ (a : α) (b : M), f =
@[simp]
theorem Finsupp.equivFunOnFinite_single {α : Type u_1} {M : Type u_5} [Zero M] [] [] (x : α) (m : M) :
Finsupp.equivFunOnFinite (Finsupp.single x m) =
@[simp]
theorem Finsupp.equivFunOnFinite_symm_single {α : Type u_1} {M : Type u_5} [Zero M] [] [] (x : α) (m : M) :
Finsupp.equivFunOnFinite.symm (Pi.single x m) =

### Declarations about update#

def Finsupp.update {α : Type u_1} {M : Type u_5} [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
• f.update a b = { support := if b = 0 then f.support.erase a else insert a f.support, toFun := Function.update (⇑f) a b, mem_support_toFun := }
Instances For
@[simp]
theorem Finsupp.coe_update {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) [] :
(f.update a b) = Function.update (⇑f) a b
@[simp]
theorem Finsupp.update_self {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) :
f.update a (f a) = f
@[simp]
theorem Finsupp.zero_update {α : Type u_1} {M : Type u_5} [Zero M] (a : α) (b : M) :
=
theorem Finsupp.support_update {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) [] [] :
(f.update a b).support = if b = 0 then f.support.erase a else insert a f.support
@[simp]
theorem Finsupp.support_update_zero {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) [] :
(f.update a 0).support = f.support.erase a
theorem Finsupp.support_update_ne_zero {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) {b : M} [] (h : b 0) :
(f.update a b).support = insert a f.support
theorem Finsupp.support_update_subset {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) {b : M} [] :
(f.update a b).support insert a f.support
theorem Finsupp.update_comm {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) {a₁ : α} {a₂ : α} (h : a₁ a₂) (m₁ : M) (m₂ : M) :
(f.update a₁ m₁).update a₂ m₂ = (f.update a₂ m₂).update a₁ m₁
@[simp]
theorem Finsupp.update_idem {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) (c : M) :
(f.update a b).update a c = f.update a c

### Declarations about erase#

def Finsupp.erase {α : Type u_1} {M : Type u_5} [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
• = { support := f.support.erase a, toFun := fun (a' : α) => if a' = a then 0 else f a', mem_support_toFun := }
Instances For
@[simp]
theorem Finsupp.support_erase {α : Type u_1} {M : Type u_5} [Zero M] [] {a : α} {f : α →₀ M} :
(Finsupp.erase a f).support = f.support.erase a
@[simp]
theorem Finsupp.erase_same {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {f : α →₀ M} :
(Finsupp.erase a f) a = 0
@[simp]
theorem Finsupp.erase_ne {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {a' : α} {f : α →₀ M} (h : a' a) :
(Finsupp.erase a f) a' = f a'
theorem Finsupp.erase_apply {α : Type u_1} {M : Type u_5} [Zero M] [] {a : α} {a' : α} {f : α →₀ M} :
(Finsupp.erase a f) a' = if a' = a then 0 else f a'
@[simp]
theorem Finsupp.erase_single {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} :
theorem Finsupp.erase_single_ne {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {a' : α} {b : M} (h : a a') :
@[simp]
theorem Finsupp.erase_of_not_mem_support {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} (haf : af.support) :
= f
@[simp]
theorem Finsupp.erase_zero {α : Type u_1} {M : Type u_5} [Zero M] (a : α) :
= 0
theorem Finsupp.erase_eq_update_zero {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) :
= f.update a 0
theorem Finsupp.erase_update_of_ne {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) {a : α} {a' : α} (ha : a a') (b : M) :
Finsupp.erase a (f.update a' b) = (Finsupp.erase a f).update a' b
theorem Finsupp.erase_idem {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) :
@[simp]
theorem Finsupp.update_erase_eq_update {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) :
(Finsupp.erase a f).update a b = f.update a b
@[simp]
theorem Finsupp.erase_update_eq_erase {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) :
Finsupp.erase a (f.update a b) =

### Declarations about onFinset#

def Finsupp.onFinset {α : Type u_1} {M : Type u_5} [Zero M] (s : ) (f : αM) (hf : ∀ (a : α), f a 0a s) :
α →₀ M

Finsupp.onFinset 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
Instances For
@[simp]
theorem Finsupp.coe_onFinset {α : Type u_1} {M : Type u_5} [Zero M] (s : ) (f : αM) (hf : ∀ (a : α), f a 0a s) :
(Finsupp.onFinset s f hf) = f
@[simp]
theorem Finsupp.onFinset_apply {α : Type u_1} {M : Type u_5} [Zero M] {s : } {f : αM} {hf : ∀ (a : α), f a 0a s} {a : α} :
(Finsupp.onFinset s f hf) a = f a
@[simp]
theorem Finsupp.support_onFinset_subset {α : Type u_1} {M : Type u_5} [Zero M] {s : } {f : αM} {hf : ∀ (a : α), f a 0a s} :
(Finsupp.onFinset s f hf).support s
theorem Finsupp.mem_support_onFinset {α : Type u_1} {M : Type u_5} [Zero M] {s : } {f : αM} (hf : ∀ (a : α), f a 0a s) {a : α} :
a (Finsupp.onFinset s f hf).support f a 0
theorem Finsupp.support_onFinset {α : Type u_1} {M : Type u_5} [Zero M] [] {s : } {f : αM} (hf : ∀ (a : α), f a 0a s) :
(Finsupp.onFinset s f hf).support = Finset.filter (fun (a : α) => f a 0) s
noncomputable def Finsupp.ofSupportFinite {α : Type u_1} {M : Type u_5} [Zero M] (f : αM) (hf : .Finite) :
α →₀ M

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

Equations
• = { support := hf.toFinset, toFun := f, mem_support_toFun := }
Instances For
theorem Finsupp.ofSupportFinite_coe {α : Type u_1} {M : Type u_5} [Zero M] {f : αM} {hf : .Finite} :
= f
instance Finsupp.instCanLift {α : Type u_1} {M : Type u_5} [Zero M] :
CanLift (αM) (α →₀ M) DFunLike.coe fun (f : αM) => .Finite
Equations
• =

### Declarations about mapRange#

def Finsupp.mapRange {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : MN) (hf : f 0 = 0) (g : α →₀ M) :
α →₀ N

The composition of f : M → N and g : α →₀ M is mapRange 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.mapRange.equiv
• Finsupp.mapRange.zeroHom
• Finsupp.mapRange.addMonoidHom
• Finsupp.mapRange.addEquiv
• Finsupp.mapRange.linearMap
• Finsupp.mapRange.linearEquiv
Equations
Instances For
@[simp]
theorem Finsupp.mapRange_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {f : MN} {hf : f 0 = 0} {g : α →₀ M} {a : α} :
(Finsupp.mapRange f hf g) a = f (g a)
@[simp]
theorem Finsupp.mapRange_zero {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {f : MN} {hf : f 0 = 0} :
@[simp]
theorem Finsupp.mapRange_id {α : Type u_1} {M : Type u_5} [Zero M] (g : α →₀ M) :
Finsupp.mapRange id g = g
theorem Finsupp.mapRange_comp {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] (f : NP) (hf : f 0 = 0) (f₂ : MN) (hf₂ : f₂ 0 = 0) (h : (f f₂) 0 = 0) (g : α →₀ M) :
Finsupp.mapRange (f f₂) h g = Finsupp.mapRange f hf (Finsupp.mapRange f₂ hf₂ g)
theorem Finsupp.support_mapRange {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {f : MN} {hf : f 0 = 0} {g : α →₀ M} :
(Finsupp.mapRange f hf g).support g.support
@[simp]
theorem Finsupp.mapRange_single {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {f : MN} {hf : f 0 = 0} {a : α} {b : M} :
theorem Finsupp.support_mapRange_of_injective {ι : Type u_4} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {e : MN} (he0 : e 0 = 0) (f : ι →₀ M) (he : ) :
(Finsupp.mapRange e he0 f).support = f.support

### Declarations about embDomain#

def Finsupp.embDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) (v : α →₀ M) :
β →₀ M

Given f : α ↪ β and v : α →₀ M, Finsupp.embDomain 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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Finsupp.support_embDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) (v : α →₀ M) :
.support = Finset.map f v.support
@[simp]
theorem Finsupp.embDomain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) :
= 0
@[simp]
theorem Finsupp.embDomain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) (v : α →₀ M) (a : α) :
(f a) = v a
theorem Finsupp.embDomain_notin_range {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) (v : α →₀ M) (a : β) (h : a) :
a = 0
theorem Finsupp.embDomain_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) :
@[simp]
theorem Finsupp.embDomain_inj {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : α β} {l₁ : α →₀ M} {l₂ : α →₀ M} :
= l₁ = l₂
@[simp]
theorem Finsupp.embDomain_eq_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : α β} {l : α →₀ M} :
= 0 l = 0
theorem Finsupp.embDomain_mapRange {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : α β) (g : MN) (p : α →₀ M) (hg : g 0 = 0) :
theorem Finsupp.single_of_embDomain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (l : α →₀ M) (f : α β) (a : β) (b : M) (hb : b 0) (h : = ) :
∃ (x : α), l = f x = a
@[simp]
theorem Finsupp.embDomain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) (a : α) (m : M) :
= Finsupp.single (f a) m

### Declarations about zipWith#

def Finsupp.zipWith {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] (f : MNP) (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, Finsupp.zipWith f hf g₁ g₂ is the finitely supported function α →₀ P satisfying zipWith f hf g₁ g₂ a = f (g₁ a) (g₂ a), which is well-defined when f 0 0 = 0.

Equations
Instances For
@[simp]
theorem Finsupp.zipWith_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] {f : MNP} {hf : f 0 0 = 0} {g₁ : α →₀ M} {g₂ : α →₀ N} {a : α} :
(Finsupp.zipWith f hf g₁ g₂) a = f (g₁ a) (g₂ a)
theorem Finsupp.support_zipWith {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] [D : ] {f : MNP} {hf : f 0 0 = 0} {g₁ : α →₀ M} {g₂ : α →₀ N} :
(Finsupp.zipWith f hf g₁ g₂).support g₁.support g₂.support
@[simp]
theorem Finsupp.zipWith_single_single {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] (f : MNP) (hf : f 0 0 = 0) (a : α) (m : M) (n : N) :

### Additive monoid structure on α →₀ M#

instance Finsupp.instAdd {α : Type u_1} {M : Type u_5} [] :
Equations
@[simp]
theorem Finsupp.coe_add {α : Type u_1} {M : Type u_5} [] (f : α →₀ M) (g : α →₀ M) :
(f + g) = f + g
theorem Finsupp.add_apply {α : Type u_1} {M : Type u_5} [] (g₁ : α →₀ M) (g₂ : α →₀ M) (a : α) :
(g₁ + g₂) a = g₁ a + g₂ a
theorem Finsupp.support_add {α : Type u_1} {M : Type u_5} [] [] {g₁ : α →₀ M} {g₂ : α →₀ M} :
(g₁ + g₂).support g₁.support g₂.support
theorem Finsupp.support_add_eq {α : Type u_1} {M : Type u_5} [] [] {g₁ : α →₀ M} {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} [] (a : α) (b₁ : M) (b₂ : M) :
Finsupp.single a (b₁ + b₂) = +
theorem Finsupp.support_single_add {α : Type u_1} {M : Type u_5} [] {a : α} {b : M} {f : α →₀ M} (ha : af.support) (hb : b 0) :
( + f).support = Finset.cons a f.support ha
theorem Finsupp.support_add_single {α : Type u_1} {M : Type u_5} [] {a : α} {b : M} {f : α →₀ M} (ha : af.support) (hb : b 0) :
(f + ).support = Finset.cons a f.support ha
instance Finsupp.instAddZeroClass {α : Type u_1} {M : Type u_5} [] :
Equations
instance Finsupp.instIsLeftCancelAdd {α : Type u_1} {M : Type u_5} [] [] :
Equations
• =
noncomputable def Finsupp.addEquivFunOnFinite {M : Type u_5} [] {ι : Type u_13} [] :
(ι →₀ M) ≃+ (ιM)

When ι is finite and M is an AddMonoid, then Finsupp.equivFunOnFinite gives an AddEquiv

Equations
Instances For
noncomputable def AddEquiv.finsuppUnique {M : Type u_5} [] {ι : Type u_13} [] :
(ι →₀ M) ≃+ M

AddEquiv between (ι →₀ M) and M, when ι has a unique element

Equations
Instances For
theorem AddEquiv.finsuppUnique_symm {M : Type u_13} [] (d : M) :
instance Finsupp.instIsRightCancelAdd {α : Type u_1} {M : Type u_5} [] [] :
Equations
• =
instance Finsupp.instIsCancelAdd {α : Type u_1} {M : Type u_5} [] [] :
Equations
• =
@[simp]
theorem Finsupp.singleAddHom_apply {α : Type u_1} {M : Type u_5} [] (a : α) (b : M) :
b =
def Finsupp.singleAddHom {α : Type u_1} {M : Type u_5} [] (a : α) :
M →+ α →₀ M

Finsupp.single as an AddMonoidHom.

See Finsupp.lsingle in LinearAlgebra/Finsupp for the stronger version as a linear map.

Equations
• = { toFun := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem Finsupp.applyAddHom_apply {α : Type u_1} {M : Type u_5} [] (a : α) (g : α →₀ M) :
g = g a
def Finsupp.applyAddHom {α : 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 LinearAlgebra/Finsupp for the stronger version as a linear map.

Equations
• = { toFun := fun (g : α →₀ M) => g a, map_zero' := , map_add' := }
Instances For
@[simp]
theorem Finsupp.coeFnAddHom_apply {α : Type u_1} {M : Type u_5} [] :
∀ (a : α →₀ M) (a_1 : α), Finsupp.coeFnAddHom a a_1 = a a_1
noncomputable def Finsupp.coeFnAddHom {α : Type u_1} {M : Type u_5} [] :
(α →₀ M) →+ αM

Coercion from a Finsupp to a function type is an AddMonoidHom.

Equations
• Finsupp.coeFnAddHom = { toFun := DFunLike.coe, map_zero' := , map_add' := }
Instances For
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) :
Finsupp.single a (f a) + = f
theorem Finsupp.erase_add_single {α : Type u_1} {M : Type u_5} [] (a : α) (f : α →₀ M) :
+ Finsupp.single a (f a) = f
@[simp]
theorem Finsupp.erase_add {α : Type u_1} {M : Type u_5} [] (a : α) (f : α →₀ M) (f' : α →₀ M) :
Finsupp.erase a (f + f') = +
@[simp]
theorem Finsupp.eraseAddHom_apply {α : Type u_1} {M : Type u_5} [] (a : α) (f : α →₀ M) :
f =
def Finsupp.eraseAddHom {α : Type u_1} {M : Type u_5} [] (a : α) :
(α →₀ M) →+ α →₀ M

Finsupp.erase as an AddMonoidHom.

Equations
• = { toFun := , map_zero' := , map_add' := }
Instances For
theorem Finsupp.induction {α : Type u_1} {M : Type u_5} [] {p : (α →₀ M)Prop} (f : α →₀ M) (h0 : p 0) (ha : ∀ (a : α) (b : M) (f : α →₀ M), af.supportb 0p fp ( + 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), af.supportb 0p fp (f + )) :
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 fp gp (f + g)) (hsingle : ∀ (a : α) (b : M), p (Finsupp.single a b)) :
p f
@[simp]
theorem Finsupp.add_closure_setOf_eq_single {α : Type u_1} {M : Type u_5} [] :
AddSubmonoid.closure {f : α →₀ M | ∃ (a : α) (b : M), f = } =
theorem Finsupp.addHom_ext {α : Type u_1} {M : Type u_5} {N : Type u_7} [] [] ⦃f : (α →₀ M) →+ N ⦃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.

theorem Finsupp.addHom_ext'_iff {α : Type u_1} {M : Type u_5} {N : Type u_7} [] [] {f : (α →₀ M) →+ N} {g : (α →₀ M) →+ N} :
f = g ∀ (x : α), f.comp = g.comp
theorem Finsupp.addHom_ext' {α : Type u_1} {M : Type u_5} {N : Type u_7} [] [] ⦃f : (α →₀ M) →+ N ⦃g : (α →₀ M) →+ N (H : ∀ (x : α), f.comp = g.comp ) :
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 AddMonoidHoms 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.mulHom_ext {α : Type u_1} {M : Type u_5} {N : Type u_7} [] [] ⦃f : Multiplicative (α →₀ M) →* N ⦃g : Multiplicative (α →₀ M) →* N (H : ∀ (x : α) (y : M), f (Multiplicative.ofAdd (Finsupp.single x y)) = g (Multiplicative.ofAdd (Finsupp.single x y))) :
f = g
theorem Finsupp.mulHom_ext'_iff {α : Type u_1} {M : Type u_5} {N : Type u_7} [] [] {f : Multiplicative (α →₀ M) →* N} {g : Multiplicative (α →₀ M) →* N} :
f = g ∀ (x : α), f.comp (AddMonoidHom.toMultiplicative ) = g.comp (AddMonoidHom.toMultiplicative )
theorem Finsupp.mulHom_ext' {α : Type u_1} {M : Type u_5} {N : Type u_7} [] [] {f : Multiplicative (α →₀ M) →* N} {g : Multiplicative (α →₀ M) →* N} (H : ∀ (x : α), f.comp (AddMonoidHom.toMultiplicative ) = g.comp (AddMonoidHom.toMultiplicative )) :
f = g
theorem Finsupp.mapRange_add {α : Type u_1} {M : Type u_5} {N : Type u_7} [] [] {f : MN} {hf : f 0 = 0} (hf' : ∀ (x y : M), f (x + y) = f x + f y) (v₁ : α →₀ M) (v₂ : α →₀ M) :
Finsupp.mapRange f hf (v₁ + v₂) = Finsupp.mapRange f hf v₁ + Finsupp.mapRange f hf v₂
theorem Finsupp.mapRange_add' {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [] [] [FunLike β M N] [] {f : β} (v₁ : α →₀ M) (v₂ : α →₀ M) :
Finsupp.mapRange f (v₁ + v₂) = Finsupp.mapRange f v₁ + Finsupp.mapRange f v₂
@[simp]
theorem Finsupp.embDomain.addMonoidHom_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [] (f : α β) (v : α →₀ M) :
def Finsupp.embDomain.addMonoidHom {α : Type u_1} {β : Type u_2} {M : Type u_5} [] (f : α β) :
(α →₀ M) →+ β →₀ M

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

Equations
• = { toFun := fun (v : α →₀ M) => , map_zero' := , map_add' := }
Instances For
@[simp]
theorem Finsupp.embDomain_add {α : Type u_1} {β : Type u_2} {M : Type u_5} [] (f : α β) (v : α →₀ M) (w : α →₀ M) :
instance Finsupp.instNatSMul {α : Type u_1} {M : Type u_5} [] :
SMul (α →₀ M)

Note the general SMul instance for Finsupp doesn't apply as ℕ is not distributive unless β i's addition is commutative.

Equations
instance Finsupp.instAddMonoid {α : Type u_1} {M : Type u_5} [] :
Equations
instance Finsupp.instAddCommMonoid {α : Type u_1} {M : Type u_5} [] :
Equations
instance Finsupp.instNeg {α : Type u_1} {G : Type u_9} [] :
Neg (α →₀ G)
Equations
@[simp]
theorem Finsupp.coe_neg {α : Type u_1} {G : Type u_9} [] (g : α →₀ G) :
(-g) = -g
theorem Finsupp.neg_apply {α : Type u_1} {G : Type u_9} [] (g : α →₀ G) (a : α) :
(-g) a = -g a
theorem Finsupp.mapRange_neg {α : Type u_1} {G : Type u_9} {H : Type u_10} [] [] {f : GH} {hf : f 0 = 0} (hf' : ∀ (x : G), f (-x) = -f x) (v : α →₀ G) :
theorem Finsupp.mapRange_neg' {α : Type u_1} {β : Type u_2} {G : Type u_9} {H : Type u_10} [] [FunLike β G H] [] {f : β} (v : α →₀ G) :
Finsupp.mapRange f (-v) = -Finsupp.mapRange f v
instance Finsupp.instSub {α : Type u_1} {G : Type u_9} [] :
Sub (α →₀ G)
Equations
@[simp]
theorem Finsupp.coe_sub {α : Type u_1} {G : Type u_9} [] (g₁ : α →₀ G) (g₂ : α →₀ G) :
(g₁ - g₂) = g₁ - g₂
theorem Finsupp.sub_apply {α : Type u_1} {G : Type u_9} [] (g₁ : α →₀ G) (g₂ : α →₀ G) (a : α) :
(g₁ - g₂) a = g₁ a - g₂ a
theorem Finsupp.mapRange_sub {α : Type u_1} {G : Type u_9} {H : Type u_10} [] [] {f : GH} {hf : f 0 = 0} (hf' : ∀ (x y : G), f (x - y) = f x - f y) (v₁ : α →₀ G) (v₂ : α →₀ G) :
Finsupp.mapRange f hf (v₁ - v₂) = Finsupp.mapRange f hf v₁ - Finsupp.mapRange f hf v₂
theorem Finsupp.mapRange_sub' {α : Type u_1} {β : Type u_2} {G : Type u_9} {H : Type u_10} [] [FunLike β G H] [] {f : β} (v₁ : α →₀ G) (v₂ : α →₀ G) :
Finsupp.mapRange f (v₁ - v₂) = Finsupp.mapRange f v₁ - Finsupp.mapRange f v₂
instance Finsupp.instIntSMul {α : Type u_1} {G : Type u_9} [] :
SMul (α →₀ G)

Note the general SMul instance for Finsupp doesn't apply as ℤ is not distributive unless β i's addition is commutative.

Equations
instance Finsupp.instAddGroup {α : Type u_1} {G : Type u_9} [] :
Equations
instance Finsupp.instAddCommGroup {α : Type u_1} {G : Type u_9} [] :
Equations