Documentation

Mathlib.Data.Finsupp.Defs

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:

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

Most of the theory assumes that the range is a commutative additive monoid. This gives us the big sum operator as a powerful way to construct Finsupp elements, which is defined in Algebra/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 #

Notations #

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

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

Implementation notes #

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

TODO #

source
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.

Instances For
source
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

Basic declarations about Finsupp #

source
instance Finsupp.instFunLike {α : Type u_1} {M : Type u_5} [Zero M] :
FunLike (α →₀ M) α M
Equations
  • Finsupp.instFunLike = { coe := Finsupp.toFun, coe_injective' := ⋯ }
source
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
source
theorem Finsupp.ext {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {g : α →₀ M} (h : ∀ (a : α), f a = g a) :
f = g
source
@[deprecated DFunLike.ext_iff]
theorem Finsupp.ext_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {g : α →₀ M} :
f = g ↔ ∀ (a : α), f a = g a
source
theorem Finsupp.ne_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {g : α →₀ M} :
f ≠ g ↔ ∃ (a : α), f a ≠ g a
source
@[deprecated DFunLike.coe_fn_eq]
theorem Finsupp.coeFn_inj {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {g : α →₀ M} :
⇑f = ⇑g ↔ f = g
source
@[deprecated DFunLike.coe_injective]
theorem Finsupp.coeFn_injective {α : Type u_1} {M : Type u_5} [Zero M] :
Function.Injective DFunLike.coe
source
@[deprecated DFunLike.congr_fun]
theorem Finsupp.congr_fun {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {g : α →₀ M} (h : f = g) (a : α) :
f a = g a
source
@[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
source
instance Finsupp.instZero {α : Type u_1} {M : Type u_5} [Zero M] :
Zero (α →₀ M)
Equations
  • Finsupp.instZero = { zero := { support := ∅, toFun := 0, mem_support_toFun := ⋯ } }
source
@[simp]
theorem Finsupp.coe_zero {α : Type u_1} {M : Type u_5} [Zero M] :
⇑0 = 0
source
theorem Finsupp.zero_apply {α : Type u_1} {M : Type u_5} [Zero M] {a : α} :
0 a = 0
source
@[simp]
theorem Finsupp.support_zero {α : Type u_1} {M : Type u_5} [Zero M] :
0.support = ∅
source
instance Finsupp.instInhabited {α : Type u_1} {M : Type u_5} [Zero M] :
Inhabited (α →₀ M)
Equations
  • Finsupp.instInhabited = { default := 0 }
source
@[simp]
theorem Finsupp.mem_support_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} :
a ∈ f.support ↔ f a ≠ 0
source
@[simp]
theorem Finsupp.fun_support_eq {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) :
Function.support ⇑f = ↑f.support
source
theorem Finsupp.not_mem_support_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} :
a ∉ f.support ↔ f a = 0
source
@[simp]
theorem Finsupp.coe_eq_zero {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
⇑f = 0 ↔ f = 0
source
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
source
@[simp]
theorem Finsupp.support_eq_empty {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
f.support = ∅ ↔ f = 0
source
theorem Finsupp.support_nonempty_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
f.support.Nonempty ↔ f ≠ 0
source
theorem Finsupp.card_support_eq_zero {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
f.support.card = 0 ↔ f = 0
source
instance Finsupp.instDecidableEq {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] [DecidableEq M] :
DecidableEq (α →₀ M)
Equations
source
theorem Finsupp.finite_support {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) :
Set.Finite (Function.support ⇑f)
source
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
source
@[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
source
@[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
source
@[simp]
theorem Finsupp.equivFunOnFinite_symm_apply_support {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] (f : α → M) :
(Finsupp.equivFunOnFinite.symm f).support = Set.Finite.toFinset ⋯
source
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 := Set.Finite.toFinset ⋯, toFun := f, mem_support_toFun := ⋯ }, left_inv := ⋯, right_inv := ⋯ }
source
@[simp]
theorem Finsupp.equivFunOnFinite_symm_coe {M : Type u_5} [Zero M] {α : Type u_13} [Finite α] (f : α →₀ M) :
Finsupp.equivFunOnFinite.symm ⇑f = f
source
@[simp]
theorem Equiv.finsuppUnique_apply {M : Type u_5} [Zero M] {ι : Type u_13} [Unique ι] :
∀ (a : ι →₀ M), Equiv.finsuppUnique a = a default
source
@[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
source
@[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
source
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
source
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
source
theorem Finsupp.unique_ext_iff {α : Type u_1} {M : Type u_5} [Zero M] [Unique α] {f : α →₀ M} {g : α →₀ M} :
f = g ↔ f default = g default

Declarations about single #

source
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
source
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
source
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
source
theorem Finsupp.single_eq_set_indicator {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} :
⇑(Finsupp.single a b) = Set.indicator {a} fun (x : α) => b
source
@[simp]
theorem Finsupp.single_eq_same {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} :
(Finsupp.single a b) a = b
source
@[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
source
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
source
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
source
@[simp]
theorem Finsupp.single_zero {α : Type u_1} {M : Type u_5} [Zero M] (a : α) :
Finsupp.single a 0 = 0
source
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
source
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}
source
theorem Finsupp.support_single_subset {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} :
(Finsupp.single a b).support ⊆ {a}
source
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}
source
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}
source
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

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

source
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'
source
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 ≠ ⊥
source
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
source
@[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
source
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₁
source
instance Finsupp.instNontrivial {α : Type u_1} {M : Type u_5} [Zero M] [Nonempty α] [Nontrivial M] :
Nontrivial (α →₀ M)
Equations
  • ⋯ = ⋯
source
theorem Finsupp.unique_single {α : Type u_1} {M : Type u_5} [Zero M] [Unique α] (x : α →₀ M) :
x = Finsupp.single default (x default)
source
@[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'
source
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)
source
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
source
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)
source
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
source
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)
source
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
source
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)
source
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
source
@[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
source
@[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 #

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

Declarations about erase #

source
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 := Finset.erase f.support a, toFun := fun (a' : α) => if a' = a then 0 else f a', mem_support_toFun := ⋯ }
source
@[simp]
theorem Finsupp.support_erase {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] {a : α} {f : α →₀ M} :
(Finsupp.erase a f).support = Finset.erase f.support a
source
@[simp]
theorem Finsupp.erase_same {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {f : α →₀ M} :
(Finsupp.erase a f) a = 0
source
@[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'
source
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'
source
@[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
source
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
source
@[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
source
@[simp]
theorem Finsupp.erase_zero {α : Type u_1} {M : Type u_5} [Zero M] (a : α) :
Finsupp.erase a 0 = 0
source
theorem Finsupp.erase_eq_update_zero {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) :
Finsupp.erase a f = Finsupp.update f a 0
source
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 (Finsupp.update f a' b) = Finsupp.update (Finsupp.erase a f) a' b
source
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
source
@[simp]
theorem Finsupp.update_erase_eq_update {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) :
Finsupp.update (Finsupp.erase a f) a b = Finsupp.update f a b
source
@[simp]
theorem Finsupp.erase_update_eq_erase {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) :
Finsupp.erase a (Finsupp.update f a b) = Finsupp.erase a f

Declarations about onFinset #

source
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
source
@[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
source
@[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
source
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
source
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
source
noncomputable def Finsupp.ofSupportFinite {α : Type u_1} {M : Type u_5} [Zero M] (f : α → M) (hf : Set.Finite (Function.support f)) :
α →₀ M

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

Equations
source
theorem Finsupp.ofSupportFinite_coe {α : Type u_1} {M : Type u_5} [Zero M] {f : α → M} {hf : Set.Finite (Function.support f)} :
⇑(Finsupp.ofSupportFinite f hf) = f
source
instance Finsupp.instCanLift {α : Type u_1} {M : Type u_5} [Zero M] :
CanLift (α → M) (α →₀ M) DFunLike.coe fun (f : α → M) => Set.Finite (Function.support f)
Equations
  • ⋯ = ⋯

Declarations about mapRange #

source
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
source
@[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)
source
@[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
source
@[simp]
theorem Finsupp.mapRange_id {α : Type u_1} {M : Type u_5} [Zero M] (g : α →₀ M) :
Finsupp.mapRange id ⋯ g = g
source
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)
source
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
source
@[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)
source
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

Declarations about embDomain #

source
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.
source
@[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
source
@[simp]
theorem Finsupp.embDomain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α ↪ β) :
Finsupp.embDomain f 0 = 0
source
@[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
source
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
source
theorem Finsupp.embDomain_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α ↪ β) :
Function.Injective (Finsupp.embDomain f)
source
@[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₂
source
@[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
source
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)
source
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
source
@[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 #

source
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
source
@[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)
source
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
source
@[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 #

source
instance Finsupp.instAdd {α : Type u_1} {M : Type u_5} [AddZeroClass M] :
Add (α →₀ M)
Equations
source
@[simp]
theorem Finsupp.coe_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f : α →₀ M) (g : α →₀ M) :
⇑(f + g) = ⇑f + ⇑g
source
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
source
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
source
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
source
@[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₂
source
instance Finsupp.instAddZeroClass {α : Type u_1} {M : Type u_5} [AddZeroClass M] :
AddZeroClass (α →₀ M)
Equations
source
instance Finsupp.instIsLeftCancelAdd {α : Type u_1} {M : Type u_5} [AddZeroClass M] [IsLeftCancelAdd M] :
IsLeftCancelAdd (α →₀ M)
Equations
  • ⋯ = ⋯
source
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 = let __spread.0 := Finsupp.equivFunOnFinite; { toEquiv := __spread.0, map_add' := ⋯ }
source
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 = let __spread.0 := Equiv.finsuppUnique; { toEquiv := __spread.0, map_add' := ⋯ }
source
theorem AddEquiv.finsuppUnique_symm {M : Type u_13} [AddZeroClass M] (d : M) :
(AddEquiv.symm AddEquiv.finsuppUnique) d = Finsupp.single () d
source
instance Finsupp.instIsRightCancelAdd {α : Type u_1} {M : Type u_5} [AddZeroClass M] [IsRightCancelAdd M] :
IsRightCancelAdd (α →₀ M)
Equations
  • ⋯ = ⋯
source
instance Finsupp.instIsCancelAdd {α : Type u_1} {M : Type u_5} [AddZeroClass M] [IsCancelAdd M] :
IsCancelAdd (α →₀ M)
Equations
  • ⋯ = ⋯
source
@[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
source
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
source
@[simp]
theorem Finsupp.applyAddHom_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (g : α →₀ M) :
(Finsupp.applyAddHom a) g = g a
source
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
source
@[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
source
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 = { toZeroHom := { toFun := DFunLike.coe, map_zero' := ⋯ }, map_add' := ⋯ }
source
theorem Finsupp.update_eq_single_add_erase {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f : α →₀ M) (a : α) (b : M) :
Finsupp.update f a b = Finsupp.single a b + Finsupp.erase a f
source
theorem Finsupp.update_eq_erase_add_single {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f : α →₀ M) (a : α) (b : M) :
Finsupp.update f a b = Finsupp.erase a f + Finsupp.single a b
source
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
source
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
source
@[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'
source
@[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
source
def Finsupp.eraseAddHom {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) :
(α →₀ M) →+ α →₀ M

Finsupp.erase as an AddMonoidHom.

Equations
source
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
source
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
source
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
source
@[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} = ⊤
source
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.

source
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 : α), AddMonoidHom.comp f (Finsupp.singleAddHom x) = AddMonoidHom.comp g (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).

source
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
source
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 : α), MonoidHom.comp f (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x)) = MonoidHom.comp g (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x))) :
f = g
source
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₂
source
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₂
source
@[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
source
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
source
@[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
source
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
source
instance Finsupp.instAddMonoid {α : Type u_1} {M : Type u_5} [AddMonoid M] :
AddMonoid (α →₀ M)
Equations
source
instance Finsupp.instAddCommMonoid {α : Type u_1} {M : Type u_5} [AddCommMonoid M] :
AddCommMonoid (α →₀ M)
Equations
source
instance Finsupp.instNeg {α : Type u_1} {G : Type u_9} [NegZeroClass G] :
Neg (α →₀ G)
Equations
source
@[simp]
theorem Finsupp.coe_neg {α : Type u_1} {G : Type u_9} [NegZeroClass G] (g : α →₀ G) :
⇑(-g) = -⇑g
source
theorem Finsupp.neg_apply {α : Type u_1} {G : Type u_9} [NegZeroClass G] (g : α →₀ G) (a : α) :
(-g) a = -g a
source
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
source
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
source
instance Finsupp.instSub {α : Type u_1} {G : Type u_9} [SubNegZeroMonoid G] :
Sub (α →₀ G)
Equations
source
@[simp]
theorem Finsupp.coe_sub {α : Type u_1} {G : Type u_9} [SubNegZeroMonoid G] (g₁ : α →₀ G) (g₂ : α →₀ G) :
⇑(g₁ - g₂) = ⇑g₁ - ⇑g₂
source
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
source
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₂
source
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₂
source
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
source
instance Finsupp.instAddGroup {α : Type u_1} {G : Type u_9} [AddGroup G] :
AddGroup (α →₀ G)
Equations
source
instance Finsupp.instAddCommGroup {α : Type u_1} {G : Type u_9} [AddCommGroup G] :
AddCommGroup (α →₀ G)
Equations
source
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
source
@[simp]
theorem Finsupp.support_neg {α : Type u_1} {G : Type u_9} [AddGroup G] (f : α →₀ G) :
(-f).support = f.support
source
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
source
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)
source
theorem Finsupp.update_eq_sub_add_single {α : Type u_1} {G : Type u_9} [AddGroup G] (f : α →₀ G) (a : α) (b : G) :
Finsupp.update f a b = f - Finsupp.single a (f a) + Finsupp.single a b