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 Mathlib.Algebra.BigOperators.Finsupp.Basic.

Many constructions based on α →₀ M are defs rather than abbrevs to avoid reusing unwanted type class 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
source
theorem Finsupp.ext {α : Type u_1} {M : Type u_5} [Zero M] {f g : α →₀ M} (h : ∀ (a : α), f a = g a) :
f = g
source
theorem Finsupp.ne_iff {α : Type u_1} {M : Type u_5} [Zero M] {f g : α →₀ M} :
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
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] :
support 0 = ∅
source
instance Finsupp.instInhabited {α : Type u_1} {M : Type u_5} [Zero M] :
Inhabited (α →₀ M)
Equations
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 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) :
(Function.support ⇑f).Finite
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
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
source
@[simp]
theorem Finsupp.equivFunOnFinite_symm_apply_support {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] (f : α → M) :
(equivFunOnFinite.symm f).support = ⋯.toFinset
source
@[simp]
theorem Finsupp.equivFunOnFinite_symm_apply_toFun {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] (f : α → M) (a✝ : α) :
(equivFunOnFinite.symm f) a✝ = f a✝
source
@[simp]
theorem Finsupp.equivFunOnFinite_apply {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] (a✝ : α →₀ M) (a : α) :
equivFunOnFinite a✝ a = a✝ a
source
@[simp]
theorem Finsupp.equivFunOnFinite_symm_coe {M : Type u_5} [Zero M] {α : Type u_13} [Finite α] (f : α →₀ M) :
equivFunOnFinite.symm ⇑f = f
source
@[simp]
theorem Finsupp.coe_equivFunOnFinite_symm {M : Type u_5} [Zero M] {α : Type u_13} [Finite α] (f : α → M) :
⇑(equivFunOnFinite.symm f) = f
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
@[simp]
theorem Equiv.finsuppUnique_symm_apply_toFun {M : Type u_5} [Zero M] {ι : Type u_13} [Unique ι] (a✝ : M) (a✝¹ : ι) :
(finsuppUnique.symm a✝) a✝¹ = a✝
source
@[simp]
theorem Equiv.finsuppUnique_apply {M : Type u_5} [Zero M] {ι : Type u_13} [Unique ι] (a✝ : ι →₀ M) :
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) :
(finsuppUnique.symm a✝).support.val = Multiset.map Subtype.val Finset.univ.val
source
theorem Finsupp.unique_ext {α : Type u_1} {M : Type u_5} [Zero M] [Unique α] {f g : α →₀ M} (h : f default = g default) :
f = g

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

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 : α} :
(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} :
mapRange f hf 0 = 0
source
@[simp]
theorem Finsupp.mapRange_id {α : Type u_1} {M : Type u_5} [Zero M] (g : α →₀ M) :
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) :
mapRange (f ∘ f₂) h g = mapRange f hf (mapRange f₂ hf₂ g)
source
@[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) :
mapRange e₁ he₁ (mapRange e₂ he₂ f) = mapRange (e₁ ∘ e₂) ⋯ f
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} :
(mapRange f hf g).support ⊆ g.support
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) :
(mapRange e he0 f).support = f.support
source
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 (mapRange e he₀) = {g : α →₀ N | ∀ (i : α), g i ∈ Set.range e}
source
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 (mapRange e he₀)

Finsupp.mapRange of a injective function is injective.

source
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 (mapRange e he₀)

Finsupp.mapRange of a surjective function is surjective.

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

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 : α} :
(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} :
(zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support

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 g : α →₀ M) :
⇑(f + g) = ⇑f + ⇑g
source
theorem Finsupp.add_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (g₁ 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₁ 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₁ g₂ : α →₀ M} (h : Disjoint g₁.support g₂.support) :
(g₁ + g₂).support = g₁.support ∪ g₂.support
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)
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
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
source
instance Finsupp.instIsRightCancelAdd {α : Type u_1} {M : Type u_5} [AddZeroClass M] [IsRightCancelAdd M] :
IsRightCancelAdd (α →₀ M)
source
instance Finsupp.instIsCancelAdd {α : Type u_1} {M : Type u_5} [AddZeroClass M] [IsCancelAdd M] :
IsCancelAdd (α →₀ M)
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.applyAddHom_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (g : α →₀ M) :
(applyAddHom a) g = g a
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
source
@[simp]
theorem Finsupp.coeFnAddHom_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a✝ : α →₀ M) (a : α) :
coeFnAddHom a✝ a = a✝ a
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₁ v₂ : α →₀ M) :
mapRange f hf (v₁ + v₂) = mapRange f hf v₁ + 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₁ v₂ : α →₀ M) :
mapRange ⇑f ⋯ (v₁ + v₂) = mapRange ⇑f ⋯ v₁ + mapRange ⇑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.addMonoidHom_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] (f : α ↪ β) (v : α →₀ M) :
(addMonoidHom f) v = embDomain f v
source
@[simp]
theorem Finsupp.embDomain_add {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] (f : α ↪ β) (v w : α →₀ M) :
embDomain f (v + w) = embDomain f v + 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) :
mapRange f hf (-v) = -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) :
mapRange ⇑f ⋯ (-v) = -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₂
source
theorem Finsupp.sub_apply {α : Type u_1} {G : Type u_9} [SubNegZeroMonoid 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₁ v₂ : α →₀ G) :
mapRange f hf (v₁ - v₂) = mapRange f hf v₁ - 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₁ v₂ : α →₀ G) :
mapRange ⇑f ⋯ (v₁ - v₂) = mapRange ⇑f ⋯ v₁ - 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
@[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} :
(f - g).support ⊆ f.support ∪ g.support