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 : Finset α

  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.

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.

def «term_→₀_» : Lean.TrailingParserDescr

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

Equations

• «term_→₀_» = Lean.ParserDescr.trailingNode `«term_→₀_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →₀ ") (Lean.ParserDescr.cat `term 25))

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' := ⋯ }

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 : Finset α) (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] : Finsupp.support 0 = ∅

instance Finsupp.instInhabited {α : Type u_1} {M : Type u_5} [Zero M] : Inhabited (α →₀ 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) : Function.support ⇑f = ↑f.support

theorem Finsupp.not_mem_support_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} : a ∉ f.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 ∧ ∀ x ∈ f.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] [DecidableEq α] [DecidableEq M] : DecidableEq (α →₀ M)

Equations

• f.instDecidableEq g = decidable_of_iff (f.support = g.support ∧ ∀ a ∈ f.support, f a = g a) ⋯

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 ↔ ∀ a ∉ s, f a = 0

def Finsupp.equivFunOnFinite {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] : (α →₀ 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 := ⋯ }

@[simp]

theorem Finsupp.equivFunOnFinite_symm_apply_toFun {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] (f : α → M) : ∀ (a : α), (Finsupp.equivFunOnFinite.symm f) a = f a

@[simp]

theorem Finsupp.equivFunOnFinite_apply {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] : ∀ (a : α →₀ M) (a_1 : α), Finsupp.equivFunOnFinite a a_1 = a a_1

@[simp]

theorem Finsupp.equivFunOnFinite_symm_apply_support {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] (f : α → M) : (Finsupp.equivFunOnFinite.symm f).support = ⋯.toFinset

@[simp]

theorem Finsupp.equivFunOnFinite_symm_coe {M : Type u_5} [Zero M] {α : Type u_13} [Finite α] (f : α →₀ M) : Finsupp.equivFunOnFinite.symm ⇑f = f

noncomputable def Equiv.finsuppUnique {M : Type u_5} [Zero M] {ι : Type u_13} [Unique ι] : (ι →₀ M) ≃ M

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

Equations

• Equiv.finsuppUnique = Finsupp.equivFunOnFinite.trans (Equiv.funUnique ι M)

@[simp]

theorem Equiv.finsuppUnique_apply {M : Type u_5} [Zero M] {ι : Type u_13} [Unique ι] : ∀ (a : ι →₀ M), Equiv.finsuppUnique a = a default

@[simp]

theorem Equiv.finsuppUnique_symm_apply_toFun {M : Type u_5} [Zero M] {ι : Type u_13} [Unique ι] : ∀ (a : M) (a_1 : ι), (Equiv.finsuppUnique.symm a) a_1 = a

@[simp]

theorem Equiv.finsuppUnique_symm_apply_support_val {M : Type u_5} [Zero M] {ι : Type u_13} [Unique ι] : ∀ (a : M), (Equiv.finsuppUnique.symm a).support.val = Multiset.map Subtype.val Finset.univ.val

theorem Finsupp.unique_ext {α : Type u_1} {M : Type u_5} [Zero M] [Unique α] {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

• Finsupp.single a b = { support := if b = 0 then ∅ else {a}, toFun := Pi.single a b, mem_support_toFun := ⋯ }

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 : 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} [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] [DecidableEq α] (a : α) (b : M) : ⇑(Finsupp.single a b) = Function.update 0 a b

theorem Finsupp.single_eq_pi_single {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] (a : α) (b : M) : ⇑(Finsupp.single a b) = Pi.single a b

@[simp]

theorem Finsupp.single_zero {α : Type u_1} {M : Type u_5} [Zero M] (a : α) : Finsupp.single a 0 = 0

theorem Finsupp.single_of_single_apply {α : Type u_1} {M : Type u_5} [Zero M] (a : α) (a' : α) (b : M) : Finsupp.single a ((Finsupp.single a' b) a) = (Finsupp.single a' (Finsupp.single a' b)) a

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 : α) : Function.Injective (Finsupp.single 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 = a → b = 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 = Finsupp.single a b ↔ 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

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) : Finsupp.single a b = Finsupp.single a' b ↔ 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} : Finsupp.single a b = 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] [Nonempty α] [Nontrivial M] : Nontrivial (α →₀ M)

Equations

• ⋯ = ⋯

theorem Finsupp.unique_single {α : Type u_1} {M : Type u_5} [Zero M] [Unique α] (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} [Unique α] {b' : M} : Finsupp.single a b = 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 : N → P) (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 = Finsupp.single a b

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 = Finsupp.single a b

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 = Finsupp.single a b

theorem Finsupp.card_support_le_one {α : Type u_1} {M : Type u_5} [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} [Zero M] [Nonempty α] {f : α →₀ M} : f.support.card ≤ 1 ↔ ∃ (a : α) (b : M), f = Finsupp.single a b

@[simp]

theorem Finsupp.equivFunOnFinite_single {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] [Finite α] (x : α) (m : M) : Finsupp.equivFunOnFinite (Finsupp.single x m) = Pi.single x m

@[simp]

theorem Finsupp.equivFunOnFinite_symm_single {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] [Finite α] (x : α) (m : M) : Finsupp.equivFunOnFinite.symm (Pi.single x m) = Finsupp.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 := ⋯ }

@[simp]

theorem Finsupp.coe_update {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) [DecidableEq α] : ⇑(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) : Finsupp.update 0 a b = Finsupp.single a b

theorem Finsupp.support_update {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) [DecidableEq α] [DecidableEq 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 : α) [DecidableEq α] : (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} [DecidableEq α] (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} [DecidableEq α] : (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

• Finsupp.erase a f = { support := f.support.erase a, toFun := fun (a' : α) => if a' = a then 0 else f a', mem_support_toFun := ⋯ }

@[simp]

theorem Finsupp.support_erase {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] {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] [DecidableEq α] {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} : Finsupp.erase a (Finsupp.single a b) = 0

theorem Finsupp.erase_single_ne {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {a' : α} {b : M} (h : a ≠ a') : Finsupp.erase a (Finsupp.single a' b) = Finsupp.single a' b

@[simp]

theorem Finsupp.erase_of_not_mem_support {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} (haf : a ∉ f.support) : Finsupp.erase a f = f

@[simp]

theorem Finsupp.erase_zero {α : Type u_1} {M : Type u_5} [Zero M] (a : α) : Finsupp.erase a 0 = 0

theorem Finsupp.erase_eq_update_zero {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) : Finsupp.erase a f = 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 : α) : Finsupp.erase a (Finsupp.erase a f) = Finsupp.erase a f

@[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) = Finsupp.erase a f

Declarations about onFinset

def Finsupp.onFinset {α : Type u_1} {M : Type u_5} [Zero M] (s : Finset α) (f : α → M) (hf : ∀ (a : α), f a ≠ 0 → a ∈ 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

• Finsupp.onFinset s f hf = { support := Finset.filter (fun (a : α) => f a ≠ 0) s, toFun := f, mem_support_toFun := ⋯ }

@[simp]

theorem Finsupp.coe_onFinset {α : Type u_1} {M : Type u_5} [Zero M] (s : Finset α) (f : α → M) (hf : ∀ (a : α), f a ≠ 0 → a ∈ s) : ⇑(Finsupp.onFinset s f hf) = f

@[simp]

theorem Finsupp.onFinset_apply {α : Type u_1} {M : Type u_5} [Zero M] {s : Finset α} {f : α → M} {hf : ∀ (a : α), f a ≠ 0 → a ∈ 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 : Finset α} {f : α → M} {hf : ∀ (a : α), f a ≠ 0 → a ∈ s} : (Finsupp.onFinset s f hf).support ⊆ s

theorem Finsupp.mem_support_onFinset {α : Type u_1} {M : Type u_5} [Zero M] {s : Finset α} {f : α → M} (hf : ∀ (a : α), f a ≠ 0 → a ∈ 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] [DecidableEq M] {s : Finset α} {f : α → M} (hf : ∀ (a : α), f a ≠ 0 → a ∈ 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 : (Function.support f).Finite) : α →₀ M

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

Equations

• Finsupp.ofSupportFinite f hf = { support := hf.toFinset, toFun := f, mem_support_toFun := ⋯ }

theorem Finsupp.ofSupportFinite_coe {α : Type u_1} {M : Type u_5} [Zero M] {f : α → M} {hf : (Function.support f).Finite} : ⇑(Finsupp.ofSupportFinite f hf) = f

instance Finsupp.instCanLift {α : Type u_1} {M : Type u_5} [Zero M] : CanLift (α → M) (α →₀ M) DFunLike.coe fun (f : α → M) => (Function.support f).Finite

Equations

• ⋯ = ⋯

Declarations about mapRange

def Finsupp.mapRange {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : M → N) (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

• Finsupp.mapRange f hf g = Finsupp.onFinset g.support (f ∘ ⇑g) ⋯

@[simp]

theorem Finsupp.mapRange_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {f : M → N} {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 : M → N} {hf : f 0 = 0} : Finsupp.mapRange f hf 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 : N → P) (hf : f 0 = 0) (f₂ : M → N) (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)

@[simp]

theorem Finsupp.mapRange_mapRange {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] (e₁ : N → P) (e₂ : M → N) (he₁ : e₁ 0 = 0) (he₂ : e₂ 0 = 0) (f : α →₀ M) : Finsupp.mapRange e₁ he₁ (Finsupp.mapRange e₂ he₂ f) = Finsupp.mapRange (e₁ ∘ e₂) ⋯ f

theorem Finsupp.support_mapRange {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {f : M → N} {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 : M → N} {hf : f 0 = 0} {a : α} {b : M} : Finsupp.mapRange f hf (Finsupp.single a b) = Finsupp.single a (f b)

theorem Finsupp.support_mapRange_of_injective {ι : Type u_4} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {e : M → N} (he0 : e 0 = 0) (f : ι →₀ M) (he : Function.Injective e) : (Finsupp.mapRange e he0 f).support = f.support

theorem Finsupp.range_mapRange {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (e : M → N) (he₀ : e 0 = 0) : Set.range (Finsupp.mapRange e he₀) = {g : α →₀ N | ∀ (i : α), g i ∈ Set.range e}

theorem Finsupp.mapRange_injective {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (e : M → N) (he₀ : e 0 = 0) (he : Function.Injective e) : Function.Injective (Finsupp.mapRange e he₀)

Finsupp.mapRange of a injective function is injective.

theorem Finsupp.mapRange_surjective {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (e : M → N) (he₀ : e 0 = 0) (he : Function.Surjective e) : Function.Surjective (Finsupp.mapRange e he₀)

Finsupp.mapRange of a surjective function is surjective.

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.

@[simp]

theorem Finsupp.support_embDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α ↪ β) (v : α →₀ M) : (Finsupp.embDomain f v).support = Finset.map f v.support

@[simp]

theorem Finsupp.embDomain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α ↪ β) : Finsupp.embDomain f 0 = 0

@[simp]

theorem Finsupp.embDomain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α ↪ β) (v : α →₀ M) (a : α) : (Finsupp.embDomain f v) (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 ∉ Set.range ⇑f) : (Finsupp.embDomain f v) a = 0

theorem Finsupp.embDomain_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α ↪ β) : Function.Injective (Finsupp.embDomain f)

@[simp]

theorem Finsupp.embDomain_inj {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : α ↪ β} {l₁ : α →₀ M} {l₂ : α →₀ M} : Finsupp.embDomain f l₁ = Finsupp.embDomain f l₂ ↔ l₁ = l₂

@[simp]

theorem Finsupp.embDomain_eq_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : α ↪ β} {l : α →₀ M} : Finsupp.embDomain f l = 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 : M → N) (p : α →₀ M) (hg : g 0 = 0) : Finsupp.embDomain f (Finsupp.mapRange g hg p) = Finsupp.mapRange g hg (Finsupp.embDomain f p)

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 : Finsupp.embDomain f l = Finsupp.single a b) : ∃ (x : α), l = Finsupp.single x b ∧ 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.embDomain f (Finsupp.single a 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 : 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, 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

• Finsupp.zipWith f hf g₁ g₂ = Finsupp.onFinset (g₁.support ∪ g₂.support) (fun (a : α) => f (g₁ a) (g₂ a)) ⋯

@[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 : M → N → P} {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 : DecidableEq α] {f : M → N → P} {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 : M → N → P) (hf : f 0 0 = 0) (a : α) (m : M) (n : N) : Finsupp.zipWith f hf (Finsupp.single a m) (Finsupp.single a n) = Finsupp.single a (f m n)

Additive monoid structure on α →₀ M

instance Finsupp.instAdd {α : Type u_1} {M : Type u_5} [AddZeroClass M] : Add (α →₀ M)

Equations

• Finsupp.instAdd = { add := Finsupp.zipWith (fun (x1 x2 : M) => x1 + x2) ⋯ }

@[simp]

theorem Finsupp.coe_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f : α →₀ M) (g : α →₀ M) : ⇑(f + g) = ⇑f + ⇑g

theorem Finsupp.add_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (g₁ : α →₀ M) (g₂ : α →₀ M) (a : α) : (g₁ + g₂) a = g₁ a + g₂ a

theorem Finsupp.support_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] [DecidableEq α] {g₁ : α →₀ M} {g₂ : α →₀ M} : (g₁ + g₂).support ⊆ g₁.support ∪ g₂.support

theorem Finsupp.support_add_eq {α : Type u_1} {M : Type u_5} [AddZeroClass M] [DecidableEq α] {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} [AddZeroClass M] (a : α) (b₁ : M) (b₂ : M) : Finsupp.single a (b₁ + b₂) = Finsupp.single a b₁ + Finsupp.single a b₂

theorem Finsupp.support_single_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] {a : α} {b : M} {f : α →₀ M} (ha : a ∉ f.support) (hb : b ≠ 0) : (Finsupp.single a b + f).support = Finset.cons a f.support ha

theorem Finsupp.support_add_single {α : Type u_1} {M : Type u_5} [AddZeroClass M] {a : α} {b : M} {f : α →₀ M} (ha : a ∉ f.support) (hb : b ≠ 0) : (f + Finsupp.single a b).support = Finset.cons a f.support ha

instance Finsupp.instAddZeroClass {α : Type u_1} {M : Type u_5} [AddZeroClass M] : AddZeroClass (α →₀ M)

Equations

• Finsupp.instAddZeroClass = Function.Injective.addZeroClass (fun (f : α →₀ M) => ⇑f) ⋯ ⋯ ⋯

instance Finsupp.instIsLeftCancelAdd {α : Type u_1} {M : Type u_5} [AddZeroClass M] [IsLeftCancelAdd M] : IsLeftCancelAdd (α →₀ M)

Equations

• ⋯ = ⋯

noncomputable def Finsupp.addEquivFunOnFinite {M : Type u_5} [AddZeroClass M] {ι : Type u_13} [Finite ι] : (ι →₀ M) ≃+ (ι → M)

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

Equations

• Finsupp.addEquivFunOnFinite = { toEquiv := Finsupp.equivFunOnFinite, map_add' := ⋯ }

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

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

Equations

• AddEquiv.finsuppUnique = { toEquiv := Equiv.finsuppUnique, map_add' := ⋯ }

theorem AddEquiv.finsuppUnique_symm {M : Type u_13} [AddZeroClass M] (d : M) : AddEquiv.finsuppUnique.symm d = Finsupp.single () d

instance Finsupp.instIsRightCancelAdd {α : Type u_1} {M : Type u_5} [AddZeroClass M] [IsRightCancelAdd M] : IsRightCancelAdd (α →₀ M)

Equations

• ⋯ = ⋯

instance Finsupp.instIsCancelAdd {α : Type u_1} {M : Type u_5} [AddZeroClass M] [IsCancelAdd M] : IsCancelAdd (α →₀ M)

Equations

• ⋯ = ⋯

def Finsupp.singleAddHom {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) : M →+ α →₀ M

Finsupp.single as an AddMonoidHom.

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

Equations

• Finsupp.singleAddHom a = { toFun := Finsupp.single a, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Finsupp.singleAddHom_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (b : M) : (Finsupp.singleAddHom a) b = Finsupp.single a b

def Finsupp.applyAddHom {α : Type u_1} {M : Type u_5} [AddZeroClass M] (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

• Finsupp.applyAddHom a = { toFun := fun (g : α →₀ M) => g a, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Finsupp.applyAddHom_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (g : α →₀ M) : (Finsupp.applyAddHom a) g = g a

noncomputable def Finsupp.coeFnAddHom {α : Type u_1} {M : Type u_5} [AddZeroClass M] : (α →₀ M) →+ α → M

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

Equations

• Finsupp.coeFnAddHom = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Finsupp.coeFnAddHom_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] : ∀ (a : α →₀ M) (a_1 : α), Finsupp.coeFnAddHom a a_1 = a a_1

theorem Finsupp.update_eq_single_add_erase {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f : α →₀ M) (a : α) (b : M) : f.update a b = Finsupp.single a b + Finsupp.erase a f

theorem Finsupp.update_eq_erase_add_single {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f : α →₀ M) (a : α) (b : M) : f.update a b = Finsupp.erase a f + Finsupp.single a b

theorem Finsupp.single_add_erase {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (f : α →₀ M) : Finsupp.single a (f a) + Finsupp.erase a f = f

theorem Finsupp.erase_add_single {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (f : α →₀ M) : Finsupp.erase a f + Finsupp.single a (f a) = f

@[simp]

theorem Finsupp.erase_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (f : α →₀ M) (f' : α →₀ M) : Finsupp.erase a (f + f') = Finsupp.erase a f + Finsupp.erase a f'

def Finsupp.eraseAddHom {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) : (α →₀ M) →+ α →₀ M

Finsupp.erase as an AddMonoidHom.

Equations

• Finsupp.eraseAddHom a = { toFun := Finsupp.erase a, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Finsupp.eraseAddHom_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (f : α →₀ M) : (Finsupp.eraseAddHom a) f = Finsupp.erase a f

theorem Finsupp.induction {α : Type u_1} {M : Type u_5} [AddZeroClass 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} [AddZeroClass 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} [AddZeroClass 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

theorem Finsupp.induction_on_max {α : Type u_1} {M : Type u_5} [AddZeroClass M] [LinearOrder α] {p : (α →₀ M) → Prop} (f : α →₀ M) (h0 : p 0) (ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (Finsupp.single a b + f)) : p f

A finitely supported function can be built by adding up single a b for increasing a.

The theorem induction_on_max₂ swaps the argument order in the sum.

theorem Finsupp.induction_on_min {α : Type u_1} {M : Type u_5} [AddZeroClass M] [LinearOrder α] {p : (α →₀ M) → Prop} (f : α →₀ M) (h0 : p 0) (ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, a < c) → b ≠ 0 → p f → p (Finsupp.single a b + f)) : p f

A finitely supported function can be built by adding up single a b for decreasing a.

The theorem induction_on_min₂ swaps the argument order in the sum.

theorem Finsupp.induction_on_max₂ {α : Type u_1} {M : Type u_5} [AddZeroClass M] [LinearOrder α] {p : (α →₀ M) → Prop} (f : α →₀ M) (h0 : p 0) (ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + Finsupp.single a b)) : p f

A finitely supported function can be built by adding up single a b for increasing a.

The theorem induction_on_max swaps the argument order in the sum.

theorem Finsupp.induction_on_min₂ {α : Type u_1} {M : Type u_5} [AddZeroClass M] [LinearOrder α] {p : (α →₀ M) → Prop} (f : α →₀ M) (h0 : p 0) (ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, a < c) → b ≠ 0 → p f → p (f + Finsupp.single a b)) : p f

A finitely supported function can be built by adding up single a b for decreasing a.

The theorem induction_on_min swaps the argument order in the sum.

@[simp]

theorem Finsupp.add_closure_setOf_eq_single {α : Type u_1} {M : Type u_5} [AddZeroClass M] : AddSubmonoid.closure {f : α →₀ M | ∃ (a : α) (b : M), f = Finsupp.single a b} = ⊤

theorem Finsupp.addHom_ext {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] ⦃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' {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] ⦃f : (α →₀ M) →+ N⦄ ⦃g : (α →₀ M) →+ N⦄ (H : ∀ (x : α), f.comp (Finsupp.singleAddHom x) = g.comp (Finsupp.singleAddHom 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 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} [AddZeroClass M] [MulOneClass N] ⦃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' {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddZeroClass M] [MulOneClass N] {f : Multiplicative (α →₀ M) →* N} {g : Multiplicative (α →₀ M) →* N} (H : ∀ (x : α), f.comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x)) = g.comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x))) : f = g

theorem Finsupp.mapRange_add {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] {f : M → N} {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} [AddZeroClass M] [AddZeroClass N] [FunLike β M N] [AddMonoidHomClass β M N] {f : β} (v₁ : α →₀ M) (v₂ : α →₀ M) : Finsupp.mapRange ⇑f ⋯ (v₁ + v₂) = Finsupp.mapRange ⇑f ⋯ v₁ + Finsupp.mapRange ⇑f ⋯ v₂

def Finsupp.embDomain.addMonoidHom {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] (f : α ↪ β) : (α →₀ M) →+ β →₀ M

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

Equations

• Finsupp.embDomain.addMonoidHom f = { toFun := fun (v : α →₀ M) => Finsupp.embDomain f v, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Finsupp.embDomain.addMonoidHom_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] (f : α ↪ β) (v : α →₀ M) : (Finsupp.embDomain.addMonoidHom f) v = Finsupp.embDomain f v

@[simp]

theorem Finsupp.embDomain_add {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] (f : α ↪ β) (v : α →₀ M) (w : α →₀ M) : Finsupp.embDomain f (v + w) = Finsupp.embDomain f v + Finsupp.embDomain f w

instance Finsupp.instNatSMul {α : Type u_1} {M : Type u_5} [AddMonoid M] : SMul ℕ (α →₀ M)

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

Equations

• Finsupp.instNatSMul = { smul := fun (n : ℕ) (v : α →₀ M) => Finsupp.mapRange (fun (x : M) => n • x) ⋯ v }

instance Finsupp.instAddMonoid {α : Type u_1} {M : Type u_5} [AddMonoid M] : AddMonoid (α →₀ M)

Equations

• Finsupp.instAddMonoid = Function.Injective.addMonoid (fun (f : α →₀ M) => ⇑f) ⋯ ⋯ ⋯ ⋯

instance Finsupp.instAddCommMonoid {α : Type u_1} {M : Type u_5} [AddCommMonoid M] : AddCommMonoid (α →₀ M)

Equations

• Finsupp.instAddCommMonoid = AddCommMonoid.mk ⋯

instance Finsupp.instNeg {α : Type u_1} {G : Type u_9} [NegZeroClass G] : Neg (α →₀ G)

Equations

• Finsupp.instNeg = { neg := Finsupp.mapRange Neg.neg ⋯ }

@[simp]

theorem Finsupp.coe_neg {α : Type u_1} {G : Type u_9} [NegZeroClass G] (g : α →₀ G) : ⇑(-g) = -⇑g

theorem Finsupp.neg_apply {α : Type u_1} {G : Type u_9} [NegZeroClass G] (g : α →₀ G) (a : α) : (-g) a = -g a

theorem Finsupp.mapRange_neg {α : Type u_1} {G : Type u_9} {H : Type u_10} [NegZeroClass G] [NegZeroClass H] {f : G → H} {hf : f 0 = 0} (hf' : ∀ (x : G), f (-x) = -f x) (v : α →₀ G) : Finsupp.mapRange f hf (-v) = -Finsupp.mapRange f hf v

theorem Finsupp.mapRange_neg' {α : Type u_1} {β : Type u_2} {G : Type u_9} {H : Type u_10} [AddGroup G] [SubtractionMonoid H] [FunLike β G H] [AddMonoidHomClass β G H] {f : β} (v : α →₀ G) : Finsupp.mapRange ⇑f ⋯ (-v) = -Finsupp.mapRange ⇑f ⋯ v

instance Finsupp.instSub {α : Type u_1} {G : Type u_9} [SubNegZeroMonoid G] : Sub (α →₀ G)

Equations

• Finsupp.instSub = { sub := Finsupp.zipWith Sub.sub ⋯ }

@[simp]

theorem Finsupp.coe_sub {α : Type u_1} {G : Type u_9} [SubNegZeroMonoid G] (g₁ : α →₀ G) (g₂ : α →₀ G) : ⇑(g₁ - g₂) = ⇑g₁ - ⇑g₂

theorem Finsupp.sub_apply {α : Type u_1} {G : Type u_9} [SubNegZeroMonoid G] (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} [SubNegZeroMonoid G] [SubNegZeroMonoid H] {f : G → H} {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} [AddGroup G] [SubtractionMonoid H] [FunLike β G H] [AddMonoidHomClass β 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} [AddGroup G] : SMul ℤ (α →₀ G)

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

Equations

• Finsupp.instIntSMul = { smul := fun (n : ℤ) (v : α →₀ G) => Finsupp.mapRange (fun (x : G) => n • x) ⋯ v }

instance Finsupp.instAddGroup {α : Type u_1} {G : Type u_9} [AddGroup G] : AddGroup (α →₀ G)

Equations

• Finsupp.instAddGroup = AddGroup.mk ⋯

instance Finsupp.instAddCommGroup {α : Type u_1} {G : Type u_9} [AddCommGroup G] : AddCommGroup (α →₀ G)

Equations

• Finsupp.instAddCommGroup = AddCommGroup.mk ⋯

theorem Finsupp.single_add_single_eq_single_add_single {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {k : α} {l : α} {m : α} {n : α} {u : M} {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} [AddGroup G] (f : α →₀ G) : (-f).support = f.support

theorem Finsupp.support_sub {α : Type u_1} {G : Type u_9} [DecidableEq α] [AddGroup G] {f : α →₀ G} {g : α →₀ G} : (f - g).support ⊆ f.support ∪ g.support

theorem Finsupp.erase_eq_sub_single {α : Type u_1} {G : Type u_9} [AddGroup G] (f : α →₀ G) (a : α) : Finsupp.erase a f = f - Finsupp.single a (f a)

theorem Finsupp.update_eq_sub_add_single {α : Type u_1} {G : Type u_9} [AddGroup G] (f : α →₀ G) (a : α) (b : G) : f.update a b = f - Finsupp.single a (f a) + Finsupp.single a b