# Miscellaneous definitions, lemmas, and constructions using finsupp #

## Main declarations #

• Finsupp.graph: the finset of input and output pairs with non-zero outputs.
• Finsupp.mapRange.equiv: Finsupp.mapRange as an equiv.
• Finsupp.mapDomain: maps the domain of a Finsupp by a function and by summing.
• Finsupp.comapDomain: postcomposition of a Finsupp with a function injective on the preimage of its support.
• Finsupp.some: restrict a finitely supported function on Option α to a finitely supported function on α.
• Finsupp.filter: filter p f is the finitely supported function that is f a if p a is true and 0 otherwise.
• Finsupp.frange: the image of a finitely supported function on its support.
• Finsupp.subtype_domain: the restriction of a finitely supported function f to a subtype.

## Implementation notes #

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

## TODO #

• This file is currently ~1600 lines long and is quite a miscellany of definitions and lemmas, so it should be divided into smaller pieces.

• Expand the list of definitions and important lemmas to the module docstring.

### Declarations about graph#

def Finsupp.graph {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) :
Finset (α × M)

The graph of a finitely supported function over its support, i.e. the finset of input and output pairs with non-zero outputs.

Equations
• f.graph = Finset.map { toFun := fun (a : α) => (a, f a), inj' := } f.support
Instances For
theorem Finsupp.mk_mem_graph_iff {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {m : M} {f : α →₀ M} :
(a, m) f.graph f a = m m 0
@[simp]
theorem Finsupp.mem_graph_iff {α : Type u_1} {M : Type u_5} [Zero M] {c : α × M} {f : α →₀ M} :
c f.graph f c.1 = c.2 c.2 0
theorem Finsupp.mk_mem_graph {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) {a : α} (ha : a f.support) :
(a, f a) f.graph
theorem Finsupp.apply_eq_of_mem_graph {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {m : M} {f : α →₀ M} (h : (a, m) f.graph) :
f a = m
@[simp]
theorem Finsupp.not_mem_graph_snd_zero {α : Type u_1} {M : Type u_5} [Zero M] (a : α) (f : α →₀ M) :
(a, 0)f.graph
@[simp]
theorem Finsupp.image_fst_graph {α : Type u_1} {M : Type u_5} [Zero M] [] (f : α →₀ M) :
Finset.image Prod.fst f.graph = f.support
theorem Finsupp.graph_injective (α : Type u_13) (M : Type u_14) [Zero M] :
Function.Injective Finsupp.graph
@[simp]
theorem Finsupp.graph_inj {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {g : α →₀ M} :
f.graph = g.graph f = g
@[simp]
theorem Finsupp.graph_zero {α : Type u_1} {M : Type u_5} [Zero M] :
@[simp]
theorem Finsupp.graph_eq_empty {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
f.graph = f = 0

### Declarations about mapRange#

@[simp]
theorem Finsupp.mapRange.equiv_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : M N) (hf : f 0 = 0) (hf' : f.symm 0 = 0) (g : α →₀ M) :
(Finsupp.mapRange.equiv f hf hf') g = Finsupp.mapRange (f) hf g
def Finsupp.mapRange.equiv {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : M N) (hf : f 0 = 0) (hf' : f.symm 0 = 0) :
(α →₀ M) (α →₀ N)

Finsupp.mapRange as an equiv.

Equations
Instances For
@[simp]
theorem Finsupp.mapRange.equiv_refl {α : Type u_1} {M : Type u_5} [Zero M] :
theorem Finsupp.mapRange.equiv_trans {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] (f : M N) (hf : f 0 = 0) (hf' : f.symm 0 = 0) (f₂ : N P) (hf₂ : f₂ 0 = 0) (hf₂' : f₂.symm 0 = 0) :
Finsupp.mapRange.equiv (f.trans f₂) = (Finsupp.mapRange.equiv f hf hf').trans (Finsupp.mapRange.equiv f₂ hf₂ hf₂')
@[simp]
theorem Finsupp.mapRange.equiv_symm {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : M N) (hf : f 0 = 0) (hf' : f.symm 0 = 0) :
(Finsupp.mapRange.equiv f hf hf').symm = Finsupp.mapRange.equiv f.symm hf' hf
@[simp]
theorem Finsupp.mapRange.zeroHom_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : ZeroHom M N) (g : α →₀ M) :
= Finsupp.mapRange f g
def Finsupp.mapRange.zeroHom {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : ZeroHom M N) :
ZeroHom (α →₀ M) (α →₀ N)

Composition with a fixed zero-preserving homomorphism is itself a zero-preserving homomorphism on functions.

Equations
• = { toFun := , map_zero' := }
Instances For
@[simp]
theorem Finsupp.mapRange.zeroHom_id {α : Type u_1} {M : Type u_5} [Zero M] :
theorem Finsupp.mapRange.zeroHom_comp {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] (f : ZeroHom N P) (f₂ : ZeroHom M N) :
Finsupp.mapRange.zeroHom (f.comp f₂) = .comp
@[simp]
theorem Finsupp.mapRange.addMonoidHom_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [] [] (f : M →+ N) (g : α →₀ M) :
= Finsupp.mapRange f g
def Finsupp.mapRange.addMonoidHom {α : Type u_1} {M : Type u_5} {N : Type u_7} [] [] (f : M →+ N) :
(α →₀ M) →+ α →₀ N

Composition with a fixed additive homomorphism is itself an additive homomorphism on functions.

Equations
• = { toFun := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem Finsupp.mapRange.addMonoidHom_id {α : Type u_1} {M : Type u_5} [] :
theorem Finsupp.mapRange.addMonoidHom_comp {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [] [] [] (f : N →+ P) (f₂ : M →+ N) :
@[simp]
theorem Finsupp.mapRange.addMonoidHom_toZeroHom {α : Type u_1} {M : Type u_5} {N : Type u_7} [] [] (f : M →+ N) :
theorem Finsupp.mapRange_multiset_sum {α : Type u_1} {M : Type u_5} {N : Type u_7} [] [] {F : Type u_13} [FunLike F M N] [] (f : F) (m : Multiset (α →₀ M)) :
Finsupp.mapRange f m.sum = (Multiset.map (fun (x : α →₀ M) => Finsupp.mapRange f x) m).sum
theorem Finsupp.mapRange_finset_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} {N : Type u_7} [] [] {F : Type u_13} [FunLike F M N] [] (f : F) (s : ) (g : ια →₀ M) :
Finsupp.mapRange f (s.sum fun (x : ι) => g x) = s.sum fun (x : ι) => Finsupp.mapRange f (g x)
@[simp]
theorem Finsupp.mapRange.addEquiv_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [] [] (f : M ≃+ N) (g : α →₀ M) :
= Finsupp.mapRange f g
def Finsupp.mapRange.addEquiv {α : Type u_1} {M : Type u_5} {N : Type u_7} [] [] (f : M ≃+ N) :
(α →₀ M) ≃+ (α →₀ N)

Finsupp.mapRange.AddMonoidHom as an equiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Finsupp.mapRange.addEquiv_refl {α : Type u_1} {M : Type u_5} [] :
theorem Finsupp.mapRange.addEquiv_trans {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [] [] [] (f : M ≃+ N) (f₂ : N ≃+ P) :
@[simp]
theorem Finsupp.mapRange.addEquiv_symm {α : Type u_1} {M : Type u_5} {N : Type u_7} [] [] (f : M ≃+ N) :
.symm =
@[simp]
theorem Finsupp.mapRange.addEquiv_toAddMonoidHom {α : Type u_1} {M : Type u_5} {N : Type u_7} [] [] (f : M ≃+ N) :
@[simp]
theorem Finsupp.mapRange.addEquiv_toEquiv {α : Type u_1} {M : Type u_5} {N : Type u_7} [] [] (f : M ≃+ N) :
=

### Declarations about equivCongrLeft#

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

Given f : α ≃ β, we can map l : α →₀ M to equivMapDomain f l : β →₀ M (computably) by mapping the support forwards and the function backwards.

Equations
• = { support := Finset.map f.toEmbedding l.support, toFun := fun (a : β) => l (f.symm a), mem_support_toFun := }
Instances For
@[simp]
theorem Finsupp.equivMapDomain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) (l : α →₀ M) (b : β) :
() b = l (f.symm b)
theorem Finsupp.equivMapDomain_symm_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) (l : β →₀ M) (a : α) :
(Finsupp.equivMapDomain f.symm l) a = l (f a)
@[simp]
theorem Finsupp.equivMapDomain_refl {α : Type u_1} {M : Type u_5} [Zero M] (l : α →₀ M) :
theorem Finsupp.equivMapDomain_refl' {α : Type u_1} {M : Type u_5} [Zero M] :
theorem Finsupp.equivMapDomain_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [Zero M] (f : α β) (g : β γ) (l : α →₀ M) :
Finsupp.equivMapDomain (f.trans g) l =
theorem Finsupp.equivMapDomain_trans' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [Zero M] (f : α β) (g : β γ) :
@[simp]
theorem Finsupp.equivMapDomain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) (a : α) (b : M) :
= Finsupp.single (f a) b
@[simp]
theorem Finsupp.equivMapDomain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : α β} :
@[simp]
theorem Finsupp.sum_equivMapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [Zero M] [] (f : α β) (l : α →₀ M) (g : βMN) :
().sum g = l.sum fun (a : α) (m : M) => g (f a) m
@[simp]
theorem Finsupp.prod_equivMapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [Zero M] [] (f : α β) (l : α →₀ M) (g : βMN) :
().prod g = l.prod fun (a : α) (m : M) => g (f a) m
def Finsupp.equivCongrLeft {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) :
(α →₀ M) (β →₀ M)

Given f : α ≃ β, the finitely supported function spaces are also in bijection: (α →₀ M) ≃ (β →₀ M).

This is the finitely-supported version of Equiv.piCongrLeft.

Equations
Instances For
@[simp]
theorem Finsupp.equivCongrLeft_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) (l : α →₀ M) :
@[simp]
theorem Finsupp.equivCongrLeft_symm {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) :
@[simp]
theorem Nat.cast_finsupp_prod {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [] (g : αM) :
(f.prod g) = f.prod fun (a : α) (b : M) => (g a b)
@[simp]
theorem Nat.cast_finsupp_sum {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [] (g : αM) :
(f.sum g) = f.sum fun (a : α) (b : M) => (g a b)
@[simp]
theorem Int.cast_finsupp_prod {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [] (g : αM) :
(f.prod g) = f.prod fun (a : α) (b : M) => (g a b)
@[simp]
theorem Int.cast_finsupp_sum {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [] (g : αM) :
(f.sum g) = f.sum fun (a : α) (b : M) => (g a b)
@[simp]
theorem Rat.cast_finsupp_sum {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [] [] (g : αM) :
(f.sum g) = f.sum fun (a : α) (b : M) => (g a b)
@[simp]
theorem Rat.cast_finsupp_prod {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [] [] (g : αM) :
(f.prod g) = f.prod fun (a : α) (b : M) => (g a b)

### Declarations about mapDomain#

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

Given f : α → β and v : α →₀ M, mapDomain f v : β →₀ M is the finitely supported function whose value at a : β is the sum of v x over all x such that f x = a.

Equations
Instances For
theorem Finsupp.mapDomain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [] {f : αβ} (hf : ) (x : α →₀ M) (a : α) :
() (f a) = x a
theorem Finsupp.mapDomain_notin_range {α : Type u_1} {β : Type u_2} {M : Type u_5} [] {f : αβ} (x : α →₀ M) (a : β) (h : a) :
() a = 0
@[simp]
theorem Finsupp.mapDomain_id {α : Type u_1} {M : Type u_5} [] {v : α →₀ M} :
= v
theorem Finsupp.mapDomain_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [] {v : α →₀ M} {f : αβ} {g : βγ} :
@[simp]
theorem Finsupp.mapDomain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [] {f : αβ} {a : α} {b : M} :
= Finsupp.single (f a) b
@[simp]
theorem Finsupp.mapDomain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [] {f : αβ} :
= 0
theorem Finsupp.mapDomain_congr {α : Type u_1} {β : Type u_2} {M : Type u_5} [] {v : α →₀ M} {f : αβ} {g : αβ} (h : xv.support, f x = g x) :
theorem Finsupp.mapDomain_add {α : Type u_1} {β : Type u_2} {M : Type u_5} [] {v₁ : α →₀ M} {v₂ : α →₀ M} {f : αβ} :
Finsupp.mapDomain f (v₁ + v₂) = +
@[simp]
theorem Finsupp.mapDomain_equiv_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [] {f : α β} (x : α →₀ M) (a : β) :
(Finsupp.mapDomain (f) x) a = x (f.symm a)
@[simp]
theorem Finsupp.mapDomain.addMonoidHom_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [] (f : αβ) (v : α →₀ M) :
def Finsupp.mapDomain.addMonoidHom {α : Type u_1} {β : Type u_2} {M : Type u_5} [] (f : αβ) :
(α →₀ M) →+ β →₀ M

Finsupp.mapDomain is an AddMonoidHom.

Equations
• = { toFun := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem Finsupp.mapDomain.addMonoidHom_id {α : Type u_1} {M : Type u_5} [] :
theorem Finsupp.mapDomain.addMonoidHom_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [] (f : βγ) (g : αβ) :
theorem Finsupp.mapDomain_finset_sum {α : Type u_1} {β : Type u_2} {ι : Type u_4} {M : Type u_5} [] {f : αβ} {s : } {v : ια →₀ M} :
Finsupp.mapDomain f (s.sum fun (i : ι) => v i) = s.sum fun (i : ι) => Finsupp.mapDomain f (v i)
theorem Finsupp.mapDomain_sum {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [] [Zero N] {f : αβ} {s : α →₀ N} {v : αNα →₀ M} :
Finsupp.mapDomain f (s.sum v) = s.sum fun (a : α) (b : N) => Finsupp.mapDomain f (v a b)
theorem Finsupp.mapDomain_support {α : Type u_1} {β : Type u_2} {M : Type u_5} [] [] {f : αβ} {s : α →₀ M} :
().support Finset.image f s.support
theorem Finsupp.mapDomain_apply' {α : Type u_1} {β : Type u_2} {M : Type u_5} [] (S : Set α) {f : αβ} (x : α →₀ M) (hS : x.support S) (hf : ) {a : α} (ha : a S) :
() (f a) = x a
theorem Finsupp.mapDomain_support_of_injOn {α : Type u_1} {β : Type u_2} {M : Type u_5} [] [] {f : αβ} (s : α →₀ M) (hf : Set.InjOn f s.support) :
().support = Finset.image f s.support
theorem Finsupp.mapDomain_support_of_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} [] [] {f : αβ} (hf : ) (s : α →₀ M) :
().support = Finset.image f s.support
theorem Finsupp.sum_mapDomain_index {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [] [] {f : αβ} {s : α →₀ M} {h : βMN} (h_zero : ∀ (b : β), h b 0 = 0) (h_add : ∀ (b : β) (m₁ m₂ : M), h b (m₁ + m₂) = h b m₁ + h b m₂) :
().sum h = s.sum fun (a : α) (m : M) => h (f a) m
theorem Finsupp.prod_mapDomain_index {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [] [] {f : αβ} {s : α →₀ M} {h : βMN} (h_zero : ∀ (b : β), h b 0 = 1) (h_add : ∀ (b : β) (m₁ m₂ : M), h b (m₁ + m₂) = h b m₁ * h b m₂) :
().prod h = s.prod fun (a : α) (m : M) => h (f a) m
@[simp]
theorem Finsupp.sum_mapDomain_index_addMonoidHom {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [] [] {f : αβ} {s : α →₀ M} (h : βM →+ N) :
(().sum fun (b : β) (m : M) => (h b) m) = s.sum fun (a : α) (m : M) => (h (f a)) m

A version of sum_mapDomain_index that takes a bundled AddMonoidHom, rather than separate linearity hypotheses.

theorem Finsupp.embDomain_eq_mapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [] (f : α β) (v : α →₀ M) :
theorem Finsupp.sum_mapDomain_index_inj {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [] [] {f : αβ} {s : α →₀ M} {h : βMN} (hf : ) :
().sum h = s.sum fun (a : α) (b : M) => h (f a) b
theorem Finsupp.prod_mapDomain_index_inj {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [] [] {f : αβ} {s : α →₀ M} {h : βMN} (hf : ) :
().prod h = s.prod fun (a : α) (b : M) => h (f a) b
theorem Finsupp.mapDomain_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} [] {f : αβ} (hf : ) :
@[simp]
theorem Finsupp.mapDomainEmbedding_apply {α : Type u_13} {β : Type u_14} (f : α β) (v : α →₀ ) :
def Finsupp.mapDomainEmbedding {α : Type u_13} {β : Type u_14} (f : α β) :

When f is an embedding we have an embedding (α →₀ ℕ) ↪ (β →₀ ℕ) given by mapDomain.

Equations
• = { toFun := , inj' := }
Instances For
theorem Finsupp.mapDomain.addMonoidHom_comp_mapRange {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [] [] (f : αβ) (g : M →+ N) :
theorem Finsupp.mapDomain_mapRange {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [] [] (f : αβ) (v : α →₀ M) (g : MN) (h0 : g 0 = 0) (hadd : ∀ (x y : M), g (x + y) = g x + g y) :

When g preserves addition, mapRange and mapDomain commute.

theorem Finsupp.sum_update_add {α : Type u_1} {β : Type u_2} {ι : Type u_4} [] [] (f : ι →₀ α) (i : ι) (a : α) (g : ιαβ) (hg : ∀ (i : ι), g i 0 = 0) (hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂) :
(f.update i a).sum g + g i (f i) = f.sum g + g i a
theorem Finsupp.mapDomain_injOn {α : Type u_1} {β : Type u_2} {M : Type u_5} [] (S : Set α) {f : αβ} (hf : ) :
Set.InjOn {w : α →₀ M | w.support S}
theorem Finsupp.equivMapDomain_eq_mapDomain {α : Type u_1} {β : Type u_2} {M : Type u_13} [] (f : α β) (l : α →₀ M) :

### Declarations about comapDomain#

@[simp]
theorem Finsupp.comapDomain_support {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : αβ) (l : β →₀ M) (hf : Set.InjOn f (f ⁻¹' l.support)) :
().support = l.support.preimage f hf
def Finsupp.comapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : αβ) (l : β →₀ M) (hf : Set.InjOn f (f ⁻¹' l.support)) :
α →₀ M

Given f : α → β, l : β →₀ M and a proof hf that f is injective on the preimage of l.support, comapDomain f l hf is the finitely supported function from α to M given by composing l with f.

Equations
• = { support := l.support.preimage f hf, toFun := fun (a : α) => l (f a), mem_support_toFun := }
Instances For
@[simp]
theorem Finsupp.comapDomain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : αβ) (l : β →₀ M) (hf : Set.InjOn f (f ⁻¹' l.support)) (a : α) :
() a = l (f a)
theorem Finsupp.sum_comapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [Zero M] [] (f : αβ) (l : β →₀ M) (g : βMN) (hf : Set.BijOn f (f ⁻¹' l.support) l.support) :
().sum (g f) = l.sum g
theorem Finsupp.eq_zero_of_comapDomain_eq_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [] (f : αβ) (l : β →₀ M) (hf : Set.BijOn f (f ⁻¹' l.support) l.support) :
= 0l = 0
theorem Finsupp.embDomain_comapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : α β} {g : β →₀ M} (hg : g.support ) :
@[simp]
theorem Finsupp.comapDomain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : αβ) (hif : optParam (Set.InjOn f (f ⁻¹' ())) ) :

Note the hif argument is needed for this to work in rw.

@[simp]
theorem Finsupp.comapDomain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : αβ) (a : α) (m : M) (hif : Set.InjOn f (f ⁻¹' (Finsupp.single (f a) m).support)) :
theorem Finsupp.comapDomain_add {α : Type u_1} {β : Type u_2} {M : Type u_5} [] {f : αβ} (v₁ : β →₀ M) (v₂ : β →₀ M) (hv₁ : Set.InjOn f (f ⁻¹' v₁.support)) (hv₂ : Set.InjOn f (f ⁻¹' v₂.support)) (hv₁₂ : Set.InjOn f (f ⁻¹' (v₁ + v₂).support)) :
Finsupp.comapDomain f (v₁ + v₂) hv₁₂ = Finsupp.comapDomain f v₁ hv₁ + Finsupp.comapDomain f v₂ hv₂
theorem Finsupp.comapDomain_add_of_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} [] {f : αβ} (hf : ) (v₁ : β →₀ M) (v₂ : β →₀ M) :
Finsupp.comapDomain f (v₁ + v₂) = +

A version of Finsupp.comapDomain_add that's easier to use.

@[simp]
theorem Finsupp.comapDomain.addMonoidHom_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [] {f : αβ} (hf : ) (x : β →₀ M) :
=
def Finsupp.comapDomain.addMonoidHom {α : Type u_1} {β : Type u_2} {M : Type u_5} [] {f : αβ} (hf : ) :
(β →₀ M) →+ α →₀ M

Finsupp.comapDomain is an AddMonoidHom.

Equations
• = { toFun := fun (x : β →₀ M) => , map_zero' := , map_add' := }
Instances For
theorem Finsupp.mapDomain_comapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [] (f : αβ) (hf : ) (l : β →₀ M) (hl : l.support ) :

### Declarations about finitely supported functions whose support is an Option type #

def Finsupp.some {α : Type u_1} {M : Type u_5} [Zero M] (f : →₀ M) :
α →₀ M

Restrict a finitely supported function on Option α to a finitely supported function on α.

Equations
Instances For
@[simp]
theorem Finsupp.some_apply {α : Type u_1} {M : Type u_5} [Zero M] (f : →₀ M) (a : α) :
f.some a = f (some a)
@[simp]
theorem Finsupp.some_zero {α : Type u_1} {M : Type u_5} [Zero M] :
@[simp]
theorem Finsupp.some_add {α : Type u_1} {M : Type u_5} [] (f : →₀ M) (g : →₀ M) :
(f + g).some = f.some + g.some
@[simp]
theorem Finsupp.some_single_none {α : Type u_1} {M : Type u_5} [Zero M] (m : M) :
(Finsupp.single none m).some = 0
@[simp]
theorem Finsupp.some_single_some {α : Type u_1} {M : Type u_5} [Zero M] (a : α) (m : M) :
(Finsupp.single (some a) m).some =
theorem Finsupp.sum_option_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [] [] (f : →₀ M) (b : MN) (h_zero : ∀ (o : ), b o 0 = 0) (h_add : ∀ (o : ) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ + b o m₂) :
f.sum b = b none (f none) + f.some.sum fun (a : α) => b (some a)
theorem Finsupp.prod_option_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [] [] (f : →₀ M) (b : MN) (h_zero : ∀ (o : ), b o 0 = 1) (h_add : ∀ (o : ) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂) :
f.prod b = b none (f none) * f.some.prod fun (a : α) => b (some a)
theorem Finsupp.sum_option_index_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} [] [] [Module R M] (f : →₀ R) (b : M) :
(f.sum fun (o : ) (r : R) => r b o) = f none b none + f.some.sum fun (a : α) (r : R) => r b (some a)

### Declarations about Finsupp.filter#

def Finsupp.filter {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [] (f : α →₀ M) :
α →₀ M

Finsupp.filter p f is the finitely supported function that is f a if p a is true and 0 otherwise.

Equations
• = { support := Finset.filter p f.support, toFun := fun (a : α) => if p a then f a else 0, mem_support_toFun := }
Instances For
theorem Finsupp.filter_apply {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [] (f : α →₀ M) (a : α) :
() a = if p a then f a else 0
theorem Finsupp.filter_eq_indicator {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [] (f : α →₀ M) :
() = {x : α | p x}.indicator f
theorem Finsupp.filter_eq_zero_iff {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [] (f : α →₀ M) :
= 0 ∀ (x : α), p xf x = 0
theorem Finsupp.filter_eq_self_iff {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [] (f : α →₀ M) :
= f ∀ (x : α), f x 0p x
@[simp]
theorem Finsupp.filter_apply_pos {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [] (f : α →₀ M) {a : α} (h : p a) :
() a = f a
@[simp]
theorem Finsupp.filter_apply_neg {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [] (f : α →₀ M) {a : α} (h : ¬p a) :
() a = 0
@[simp]
theorem Finsupp.support_filter {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [] (f : α →₀ M) :
().support = Finset.filter p f.support
theorem Finsupp.filter_zero {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [] :
= 0
@[simp]
theorem Finsupp.filter_single_of_pos {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [] {a : α} {b : M} (h : p a) :
@[simp]
theorem Finsupp.filter_single_of_neg {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [] {a : α} {b : M} (h : ¬p a) :
theorem Finsupp.sum_filter_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] (p : αProp) [] (f : α →₀ M) [] (g : αMN) :
().sum g = ().support.sum fun (x : α) => g x (f x)
theorem Finsupp.prod_filter_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] (p : αProp) [] (f : α →₀ M) [] (g : αMN) :
().prod g = ().support.prod fun (x : α) => g x (f x)
@[simp]
theorem Finsupp.sum_filter_add_sum_filter_not {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] (p : αProp) [] (f : α →₀ M) [] (g : αMN) :
().sum g + (Finsupp.filter (fun (a : α) => ¬p a) f).sum g = f.sum g
@[simp]
theorem Finsupp.prod_filter_mul_prod_filter_not {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] (p : αProp) [] (f : α →₀ M) [] (g : αMN) :
().prod g * (Finsupp.filter (fun (a : α) => ¬p a) f).prod g = f.prod g
@[simp]
theorem Finsupp.sum_sub_sum_filter {α : Type u_1} {M : Type u_5} {G : Type u_9} [Zero M] (p : αProp) [] (f : α →₀ M) [] (g : αMG) :
f.sum g - ().sum g = (Finsupp.filter (fun (a : α) => ¬p a) f).sum g
@[simp]
theorem Finsupp.prod_div_prod_filter {α : Type u_1} {M : Type u_5} {G : Type u_9} [Zero M] (p : αProp) [] (f : α →₀ M) [] (g : αMG) :
f.prod g / ().prod g = (Finsupp.filter (fun (a : α) => ¬p a) f).prod g
theorem Finsupp.filter_pos_add_filter_neg {α : Type u_1} {M : Type u_5} [] (f : α →₀ M) (p : αProp) [] :
+ Finsupp.filter (fun (a : α) => ¬p a) f = f

### Declarations about frange#

def Finsupp.frange {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) :

frange f is the image of f on the support of f.

Equations
Instances For
theorem Finsupp.mem_frange {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {y : M} :
y f.frange y 0 ∃ (x : α), f x = y
theorem Finsupp.zero_not_mem_frange {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
0f.frange
theorem Finsupp.frange_single {α : Type u_1} {M : Type u_5} [Zero M] {x : α} {y : M} :
().frange {y}

### Declarations about Finsupp.subtypeDomain#

def Finsupp.subtypeDomain {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) (f : α →₀ M) :

subtypeDomain p f is the restriction of the finitely supported function f to subtype p.

Equations
• = { support := Finset.subtype p f.support, toFun := f Subtype.val, mem_support_toFun := }
Instances For
@[simp]
theorem Finsupp.support_subtypeDomain {α : Type u_1} {M : Type u_5} [Zero M] {p : αProp} [D : ] {f : α →₀ M} :
().support = Finset.subtype p f.support
@[simp]
theorem Finsupp.subtypeDomain_apply {α : Type u_1} {M : Type u_5} [Zero M] {p : αProp} {a : } {v : α →₀ M} :
() a = v a
@[simp]
theorem Finsupp.subtypeDomain_zero {α : Type u_1} {M : Type u_5} [Zero M] {p : αProp} :
theorem Finsupp.subtypeDomain_eq_zero_iff' {α : Type u_1} {M : Type u_5} [Zero M] {p : αProp} {f : α →₀ M} :
∀ (x : α), p xf x = 0
theorem Finsupp.subtypeDomain_eq_zero_iff {α : Type u_1} {M : Type u_5} [Zero M] {p : αProp} {f : α →₀ M} (hf : xf.support, p x) :
f = 0
theorem Finsupp.sum_subtypeDomain_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] {p : αProp} [] {v : α →₀ M} {h : αMN} (hp : xv.support, p x) :
(().sum fun (a : ) (b : M) => h (a) b) = v.sum h
theorem Finsupp.prod_subtypeDomain_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] {p : αProp} [] {v : α →₀ M} {h : αMN} (hp : xv.support, p x) :
(().prod fun (a : ) (b : M) => h (a) b) = v.prod h
@[simp]
theorem Finsupp.subtypeDomain_add {α : Type u_1} {M : Type u_5} [] {p : αProp} {v : α →₀ M} {v' : α →₀ M} :
def Finsupp.subtypeDomainAddMonoidHom {α : Type u_1} {M : Type u_5} [] {p : αProp} :
(α →₀ M) →+ →₀ M

subtypeDomain but as an AddMonoidHom.

Equations
• Finsupp.subtypeDomainAddMonoidHom = { toFun := , map_zero' := , map_add' := }
Instances For
def Finsupp.filterAddHom {α : Type u_1} {M : Type u_5} [] (p : αProp) [] :
(α →₀ M) →+ α →₀ M

Finsupp.filter as an AddMonoidHom.

Equations
• = { toFun := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem Finsupp.filter_add {α : Type u_1} {M : Type u_5} [] {p : αProp} [] {v : α →₀ M} {v' : α →₀ M} :
Finsupp.filter p (v + v') = +
theorem Finsupp.subtypeDomain_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} [] {p : αProp} {s : } {h : ια →₀ M} :
Finsupp.subtypeDomain p (s.sum fun (c : ι) => h c) = s.sum fun (c : ι) => Finsupp.subtypeDomain p (h c)
theorem Finsupp.subtypeDomain_finsupp_sum {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [] {p : αProp} [Zero N] {s : β →₀ N} {h : βNα →₀ M} :
Finsupp.subtypeDomain p (s.sum h) = s.sum fun (c : β) (d : N) => Finsupp.subtypeDomain p (h c d)
theorem Finsupp.filter_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} [] {p : αProp} [] (s : ) (f : ια →₀ M) :
Finsupp.filter p (s.sum fun (a : ι) => f a) = s.sum fun (a : ι) => Finsupp.filter p (f a)
theorem Finsupp.filter_eq_sum {α : Type u_1} {M : Type u_5} [] (p : αProp) [] (f : α →₀ M) :
= (Finset.filter p f.support).sum fun (i : α) => Finsupp.single i (f i)
@[simp]
theorem Finsupp.subtypeDomain_neg {α : Type u_1} {G : Type u_9} [] {p : αProp} {v : α →₀ G} :
@[simp]
theorem Finsupp.subtypeDomain_sub {α : Type u_1} {G : Type u_9} [] {p : αProp} {v : α →₀ G} {v' : α →₀ G} :
@[simp]
theorem Finsupp.single_neg {α : Type u_1} {G : Type u_9} [] (a : α) (b : G) :
@[simp]
theorem Finsupp.single_sub {α : Type u_1} {G : Type u_9} [] (a : α) (b₁ : G) (b₂ : G) :
Finsupp.single a (b₁ - b₂) = -
@[simp]
theorem Finsupp.erase_neg {α : Type u_1} {G : Type u_9} [] (a : α) (f : α →₀ G) :
@[simp]
theorem Finsupp.erase_sub {α : Type u_1} {G : Type u_9} [] (a : α) (f₁ : α →₀ G) (f₂ : α →₀ G) :
Finsupp.erase a (f₁ - f₂) = -
@[simp]
theorem Finsupp.filter_neg {α : Type u_1} {G : Type u_9} [] (p : αProp) [] (f : α →₀ G) :
@[simp]
theorem Finsupp.filter_sub {α : Type u_1} {G : Type u_9} [] (p : αProp) [] (f₁ : α →₀ G) (f₂ : α →₀ G) :
Finsupp.filter p (f₁ - f₂) = -
theorem Finsupp.mem_support_multiset_sum {α : Type u_1} {M : Type u_5} [] {s : Multiset (α →₀ M)} (a : α) :
a s.sum.supportfs, a f.support
theorem Finsupp.mem_support_finset_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} [] {s : } {h : ια →₀ M} (a : α) (ha : a (s.sum fun (c : ι) => h c).support) :
cs, a (h c).support

### Declarations about curry and uncurry#

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

Given a finitely supported function f from a product type α × β to γ, curry f is the "curried" finitely supported function from α to the type of finitely supported functions from β to γ.

Equations
Instances For
@[simp]
theorem Finsupp.curry_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [] (f : α × β →₀ M) (x : α) (y : β) :
(f.curry x) y = f (x, y)
theorem Finsupp.sum_curry_index {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [] [] (f : α × β →₀ M) (g : αβMN) (hg₀ : ∀ (a : α) (b : β), g a b 0 = 0) (hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁) :
(f.curry.sum fun (a : α) (f : β →₀ M) => f.sum (g a)) = f.sum fun (p : α × β) (c : M) => g p.1 p.2 c
def Finsupp.uncurry {α : Type u_1} {β : Type u_2} {M : Type u_5} [] (f : α →₀ β →₀ M) :
α × β →₀ M

Given a finitely supported function f from α to the type of finitely supported functions from β to M, uncurry f is the "uncurried" finitely supported function from α × β to M.

Equations
• f.uncurry = f.sum fun (a : α) (g : β →₀ M) => g.sum fun (b : β) (c : M) => Finsupp.single (a, b) c
Instances For
def Finsupp.finsuppProdEquiv {α : Type u_1} {β : Type u_2} {M : Type u_5} [] :
(α × β →₀ M) (α →₀ β →₀ M)

finsuppProdEquiv defines the Equiv between ((α × β) →₀ M) and (α →₀ (β →₀ M)) given by currying and uncurrying.

Equations
• Finsupp.finsuppProdEquiv = { toFun := Finsupp.curry, invFun := Finsupp.uncurry, left_inv := , right_inv := }
Instances For
theorem Finsupp.filter_curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [] (f : α × β →₀ M) (p : αProp) [] :
(Finsupp.filter (fun (a : α × β) => p a.1) f).curry = Finsupp.filter p f.curry
theorem Finsupp.support_curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [] [] (f : α × β →₀ M) :
f.curry.support Finset.image Prod.fst f.support

### Declarations about finitely supported functions whose support is a Sum type #

def Finsupp.sumElim {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α →₀ γ) (g : β →₀ γ) :
α β →₀ γ

Finsupp.sumElim f g maps inl x to f x and inr y to g y.

Equations
Instances For
@[simp]
theorem Finsupp.coe_sumElim {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α →₀ γ) (g : β →₀ γ) :
(f.sumElim g) = Sum.elim f g
theorem Finsupp.sumElim_apply {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α →₀ γ) (g : β →₀ γ) (x : α β) :
(f.sumElim g) x = Sum.elim (f) (g) x
theorem Finsupp.sumElim_inl {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α →₀ γ) (g : β →₀ γ) (x : α) :
(f.sumElim g) () = f x
theorem Finsupp.sumElim_inr {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α →₀ γ) (g : β →₀ γ) (x : β) :
(f.sumElim g) () = g x
@[simp]
theorem Finsupp.sumFinsuppEquivProdFinsupp_symm_apply {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (fg : (α →₀ γ) × (β →₀ γ)) :
Finsupp.sumFinsuppEquivProdFinsupp.symm fg = fg.1.sumElim fg.2
@[simp]
theorem Finsupp.sumFinsuppEquivProdFinsupp_apply {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α β →₀ γ) :
Finsupp.sumFinsuppEquivProdFinsupp f = (Finsupp.comapDomain Sum.inl f , Finsupp.comapDomain Sum.inr f )
def Finsupp.sumFinsuppEquivProdFinsupp {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] :
(α β →₀ γ) (α →₀ γ) × (β →₀ γ)

The equivalence between (α ⊕ β) →₀ γ and (α →₀ γ) × (β →₀ γ).

This is the Finsupp version of Equiv.sum_arrow_equiv_prod_arrow.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Finsupp.fst_sumFinsuppEquivProdFinsupp {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α β →₀ γ) (x : α) :
(Finsupp.sumFinsuppEquivProdFinsupp f).1 x = f ()
theorem Finsupp.snd_sumFinsuppEquivProdFinsupp {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α β →₀ γ) (y : β) :
(Finsupp.sumFinsuppEquivProdFinsupp f).2 y = f ()
theorem Finsupp.sumFinsuppEquivProdFinsupp_symm_inl {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (fg : (α →₀ γ) × (β →₀ γ)) (x : α) :
(Finsupp.sumFinsuppEquivProdFinsupp.symm fg) () = fg.1 x
theorem Finsupp.sumFinsuppEquivProdFinsupp_symm_inr {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (fg : (α →₀ γ) × (β →₀ γ)) (y : β) :
(Finsupp.sumFinsuppEquivProdFinsupp.symm fg) () = fg.2 y
@[simp]
theorem Finsupp.sumFinsuppAddEquivProdFinsupp_apply {M : Type u_5} [] {α : Type u_13} {β : Type u_14} (f : α β →₀ M) :
Finsupp.sumFinsuppAddEquivProdFinsupp f = (Finsupp.comapDomain Sum.inl f , Finsupp.comapDomain Sum.inr f )
@[simp]
theorem Finsupp.sumFinsuppAddEquivProdFinsupp_symm_apply {M : Type u_5} [] {α : Type u_13} {β : Type u_14} (fg : (α →₀ M) × (β →₀ M)) :
def Finsupp.sumFinsuppAddEquivProdFinsupp {M : Type u_5} [] {α : Type u_13} {β : Type u_14} :
(α β →₀ M) ≃+ (α →₀ M) × (β →₀ M)

The additive equivalence between (α ⊕ β) →₀ M and (α →₀ M) × (β →₀ M).

This is the Finsupp version of Equiv.sum_arrow_equiv_prod_arrow.

Equations
• Finsupp.sumFinsuppAddEquivProdFinsupp = let __src := Finsupp.sumFinsuppEquivProdFinsupp; { toEquiv := __src, map_add' := }
Instances For
theorem Finsupp.fst_sumFinsuppAddEquivProdFinsupp {M : Type u_5} [] {α : Type u_13} {β : Type u_14} (f : α β →₀ M) (x : α) :
(Finsupp.sumFinsuppAddEquivProdFinsupp f).1 x = f ()
theorem Finsupp.snd_sumFinsuppAddEquivProdFinsupp {M : Type u_5} [] {α : Type u_13} {β : Type u_14} (f : α β →₀ M) (y : β) :
(Finsupp.sumFinsuppAddEquivProdFinsupp f).2 y = f ()
theorem Finsupp.sumFinsuppAddEquivProdFinsupp_symm_inl {M : Type u_5} [] {α : Type u_13} {β : Type u_14} (fg : (α →₀ M) × (β →₀ M)) (x : α) :
(Finsupp.sumFinsuppAddEquivProdFinsupp.symm fg) () = fg.1 x
theorem Finsupp.sumFinsuppAddEquivProdFinsupp_symm_inr {M : Type u_5} [] {α : Type u_13} {β : Type u_14} (fg : (α →₀ M) × (β →₀ M)) (y : β) :
(Finsupp.sumFinsuppAddEquivProdFinsupp.symm fg) () = fg.2 y

### Declarations about scalar multiplication #

@[simp]
theorem Finsupp.single_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] [] [] (a : α) (b : α) (f : αM) (r : R) :
() b f a = (Finsupp.single a (r f b)) b
def Finsupp.comapSMul {α : Type u_1} {M : Type u_5} {G : Type u_9} [] [] [] :
SMul G (α →₀ M)

Scalar multiplication acting on the domain.

This is not an instance as it would conflict with the action on the range. See the instance_diamonds test for examples of such conflicts.

Equations
Instances For
theorem Finsupp.comapSMul_def {α : Type u_1} {M : Type u_5} {G : Type u_9} [] [] [] (g : G) (f : α →₀ M) :
g f = Finsupp.mapDomain (fun (x : α) => g x) f
@[simp]
theorem Finsupp.comapSMul_single {α : Type u_1} {M : Type u_5} {G : Type u_9} [] [] [] (g : G) (a : α) (b : M) :
def Finsupp.comapMulAction {α : Type u_1} {M : Type u_5} {G : Type u_9} [] [] [] :
MulAction G (α →₀ M)

Finsupp.comapSMul is multiplicative

Equations
• Finsupp.comapMulAction =
Instances For
def Finsupp.comapDistribMulAction {α : Type u_1} {M : Type u_5} {G : Type u_9} [] [] [] :

Finsupp.comapSMul is distributive

Equations
• Finsupp.comapDistribMulAction =
Instances For
@[simp]
theorem Finsupp.comapSMul_apply {α : Type u_1} {M : Type u_5} {G : Type u_9} [] [] [] (g : G) (f : α →₀ M) (a : α) :
(g f) a = f (g⁻¹ a)

When G is a group, Finsupp.comapSMul acts by precomposition with the action of g⁻¹.

instance Finsupp.smulZeroClass {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] [] :
Equations
• Finsupp.smulZeroClass =

Throughout this section, some Monoid and Semiring arguments are specified with {} instead of []. See note [implicit instance arguments].

@[simp]
theorem Finsupp.coe_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] [] (b : R) (v : α →₀ M) :
(b v) = b v
theorem Finsupp.smul_apply {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] [] (b : R) (v : α →₀ M) (a : α) :
(b v) a = b v a
theorem IsSMulRegular.finsupp {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] [] {k : R} (hk : ) :
instance Finsupp.faithfulSMul {α : Type u_1} {M : Type u_5} {R : Type u_11} [] [Zero M] [] [] :
Equations
• =
instance Finsupp.instSMulWithZero {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero R] [Zero M] [] :
Equations
• Finsupp.instSMulWithZero =
instance Finsupp.distribSMul (α : Type u_1) (M : Type u_5) {R : Type u_11} [] [] :
Equations
instance Finsupp.distribMulAction (α : Type u_1) (M : Type u_5) {R : Type u_11} [] [] [] :
Equations
• = let __src := ;
instance Finsupp.isScalarTower (α : Type u_1) (M : Type u_5) {R : Type u_11} {S : Type u_12} [Zero M] [] [] [SMul R S] [] :
Equations
• =
instance Finsupp.smulCommClass (α : Type u_1) (M : Type u_5) {R : Type u_11} {S : Type u_12} [Zero M] [] [] [] :
Equations
• =
instance Finsupp.isCentralScalar (α : Type u_1) (M : Type u_5) {R : Type u_11} [Zero M] [] [] [] :
Equations
• =
instance Finsupp.module (α : Type u_1) (M : Type u_5) {R : Type u_11} [] [] [Module R M] :
Module R (α →₀ M)
Equations
theorem Finsupp.support_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} [] [] {b : R} {g : α →₀ M} :
(b g).support g.support
@[simp]
theorem Finsupp.support_smul_eq {α : Type u_1} {M : Type u_5} {R : Type u_11} [] [] [Module R M] [] {b : R} (hb : b 0) {g : α →₀ M} :
(b g).support = g.support
@[simp]
theorem Finsupp.filter_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} {p : αProp} [] :
∀ {x : } [inst : ] [inst_1 : ] {b : R} {v : α →₀ M}, Finsupp.filter p (b v) = b
theorem Finsupp.mapDomain_smul {α : Type u_1} {β : Type u_2} {M : Type u_5} {R : Type u_11} :
∀ {x : } [inst : ] [inst_1 : ] {f : αβ} (b : R) (v : α →₀ M), Finsupp.mapDomain f (b v) = b
@[simp]
theorem Finsupp.smul_single {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] [] (c : R) (a : α) (b : M) :
theorem Finsupp.smul_single' {α : Type u_1} {R : Type u_11} :
∀ {x : } (c : R) (a : α) (b : R), c = Finsupp.single a (c * b)
theorem Finsupp.mapRange_smul {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} :
∀ {x : } [inst : ] [inst_1 : ] [inst_2 : ] [inst_3 : ] {f : MN} {hf : f 0 = 0} (c : R) (v : α →₀ M), (∀ (x_1 : M), f (c x_1) = c f x_1)Finsupp.mapRange f hf (c v) = c Finsupp.mapRange f hf v
theorem Finsupp.smul_single_one {α : Type u_1} {R : Type u_11} [] (a : α) (b : R) :
b =
theorem Finsupp.comapDomain_smul {α : Type u_1} {β : Type u_2} {M : Type u_5} {R : Type u_11} [] [] [] {f : αβ} (r : R) (v : β →₀ M) (hfv : Set.InjOn f (f ⁻¹' v.support)) (hfrv : optParam (Set.InjOn f (f ⁻¹' (r v).support)) ) :
theorem Finsupp.comapDomain_smul_of_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} {R : Type u_11} [] [] [] {f : αβ} (hf : ) (r : R) (v : β →₀ M) :
Finsupp.comapDomain f (r v) = r

A version of Finsupp.comapDomain_smul that's easier to use.

theorem Finsupp.sum_smul_index {α : Type u_1} {M : Type u_5} {R : Type u_11} [] [] {g : α →₀ R} {b : R} {h : αRM} (h0 : ∀ (i : α), h i 0 = 0) :
(b g).sum h = g.sum fun (i : α) (a : R) => h i (b * a)
theorem Finsupp.sum_smul_index' {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} [] [] [] {g : α →₀ M} {b : R} {h : αMN} (h0 : ∀ (i : α), h i 0 = 0) :
(b g).sum h = g.sum fun (i : α) (c : M) => h i (b c)
theorem Finsupp.sum_smul_index_addMonoidHom {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} [] [] [] {g : α →₀ M} {b : R} {h : αM →+ N} :
((b g).sum fun (a : α) => (h a)) = g.sum fun (i : α) (c : M) => (h i) (b c)

A version of Finsupp.sum_smul_index' for bundled additive maps.

instance Finsupp.noZeroSMulDivisors {M : Type u_5} {R : Type u_11} [] [] [Module R M] {ι : Type u_13} [] :
Equations
• =
def Finsupp.DistribMulActionHom.single {α : Type u_1} {M : Type u_5} {R : Type u_11} [] [] [] (a : α) :
M →+[R] α →₀ M

Finsupp.single as a DistribMulActionSemiHom.

See also Finsupp.lsingle for the version as a linear map.

Equations
• = let __src := ; { toFun := (__src).toFun, map_smul' := , map_zero' := , map_add' := }
Instances For
theorem Finsupp.distribMulActionHom_ext {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} [] [] [] [] [] {f : (α →₀ M) →+[R] N} {g : (α →₀ M) →+[R] N} (h : ∀ (a : α) (m : M), f () = g ()) :
f = g
theorem Finsupp.distribMulActionHom_ext' {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} [] [] [] [] [] {f : (α →₀ M) →+[R] N} {g : (α →₀ M) →+[R] N} (h : ∀ (a : α), f.comp = g.comp ) :
f = g

See note [partially-applied ext lemmas].

instance Finsupp.uniqueOfRight {α : Type u_1} {R : Type u_11} [Zero R] [] :
Unique (α →₀ R)

The Finsupp version of Pi.unique.

Equations
• Finsupp.uniqueOfRight = .unique
instance Finsupp.uniqueOfLeft {α : Type u_1} {R : Type u_11} [Zero R] [] :
Unique (α →₀ R)

The Finsupp version of Pi.uniqueOfIsEmpty.

Equations
• Finsupp.uniqueOfLeft = .unique
@[simp]
theorem Finsupp.piecewise_support {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [] (f : →₀ M) (g : { a : α // ¬P a } →₀ M) :
(f.piecewise g).support = (Finset.map f.support).disjUnion (Finset.map (Function.Embedding.subtype fun (a : α) => ¬P a) g.support)
@[simp]
theorem Finsupp.piecewise_toFun {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [] (f : →₀ M) (g : { a : α // ¬P a } →₀ M) (a : α) :
(f.piecewise g) a = if h : P a then f a, h else g a, h
def Finsupp.piecewise {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [] (f : →₀ M) (g : { a : α // ¬P a } →₀ M) :
α →₀ M

Combine finitely supported functions over {a // P a} and {a // ¬P a}, by case-splitting on P a.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Finsupp.subtypeDomain_piecewise {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [] (f : →₀ M) (g : { a : α // ¬P a } →₀ M) :
Finsupp.subtypeDomain P (f.piecewise g) = f
@[simp]
theorem Finsupp.subtypeDomain_not_piecewise {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [] (f : →₀ M) (g : { a : α // ¬P a } →₀ M) :
Finsupp.subtypeDomain (fun (x : α) => ¬P x) (f.piecewise g) = g
@[simp]
theorem Finsupp.extendDomain_toFun {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [] (f : →₀ M) (a : α) :
f.extendDomain a = if h : P a then f a, h else 0
@[simp]
theorem Finsupp.extendDomain_support {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [] (f : →₀ M) :
f.extendDomain.support = Finset.map f.support
def Finsupp.extendDomain {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [] (f : →₀ M) :
α →₀ M

Extend the domain of a Finsupp by using 0 where P x does not hold.

Equations
• f.extendDomain = f.piecewise 0
Instances For
theorem Finsupp.extendDomain_eq_embDomain_subtype {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [] (f : →₀ M) :
f.extendDomain =
theorem Finsupp.support_extendDomain_subset {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [] (f : →₀ M) :
f.extendDomain.support {x : α | P x}
@[simp]
theorem Finsupp.subtypeDomain_extendDomain {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [] (f : →₀ M) :
Finsupp.subtypeDomain P f.extendDomain = f
theorem Finsupp.extendDomain_subtypeDomain {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [] (f : α →₀ M) (hf : af.support, P a) :
().extendDomain = f
@[simp]
theorem Finsupp.extendDomain_single {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [] (a : ) (m : M) :
().extendDomain = Finsupp.single (a) m
def Finsupp.restrictSupportEquiv {α : Type u_1} (s : Set α) (M : Type u_13) [] :
{ f : α →₀ M // f.support s } (s →₀ M)

Given an AddCommMonoid M and s : Set α, restrictSupportEquiv s M is the Equiv between the subtype of finitely supported functions with support contained in s and the type of finitely supported functions from s.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Finsupp.domCongr_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [] (e : α β) (l : α →₀ M) :
() l =
def Finsupp.domCongr {α : Type u_1} {β : Type u_2} {M : Type u_5} [] (e : α β) :
(α →₀ M) ≃+ (β →₀ M)

Given AddCommMonoid M and e : α ≃ β, domCongr e is the corresponding Equiv between α →₀ M and β →₀ M.

This is Finsupp.equivCongrLeft as an AddEquiv.

Equations
Instances For
@[simp]
theorem Finsupp.domCongr_refl {α : Type u_1} {M : Type u_5} [] :
@[simp]
theorem Finsupp.domCongr_symm {α : Type u_1} {β : Type u_2} {M : Type u_5} [] (e : α β) :
().symm = Finsupp.domCongr e.symm
@[simp]
theorem Finsupp.domCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [] (e : α β) (f : β γ) :
().trans () = Finsupp.domCongr (e.trans f)

### Declarations about sigma types #

def Finsupp.split {ι : Type u_4} {M : Type u_5} {αs : ιType u_13} [Zero M] (l : (i : ι) × αs i →₀ M) (i : ι) :
αs i →₀ M

Given l, a finitely supported function from the sigma type Σ (i : ι), αs i to M and an index element i : ι, split l i is the ith component of l, a finitely supported function from as i to M.

This is the Finsupp version of Sigma.curry.

Equations
• l.split i =
Instances For
theorem Finsupp.split_apply {ι : Type u_4} {M : Type u_5} {αs : ιType u_13} [Zero M] (l : (i : ι) × αs i →₀ M) (i : ι) (x : αs i) :
(l.split i) x = l i, x
def Finsupp.splitSupport {ι : Type u_4} {M : Type u_5} {αs : ιType u_13} [Zero M] (l : (i : ι) × αs i →₀ M) :

Given l, a finitely supported function from the sigma type Σ (i : ι), αs i to β, split_support l is the finset of indices in ι that appear in the support of l.

Equations
Instances For
theorem Finsupp.mem_splitSupport_iff_nonzero {ι : Type u_4} {M : Type u_5} {αs : ιType u_13} [Zero M] (l : (i : ι) × αs i →₀ M) (i : ι) :
i l.splitSupport l.split i 0
def Finsupp.splitComp {ι : Type u_4} {M : Type u_5} {N : Type u_7} {αs : ιType u_13} [Zero M] (l : (i : ι) × αs i →₀ M) [Zero N] (g : (i : ι) → (αs i →₀ M)N) (hg : ∀ (i : ι) (x : αs i →₀ M), x = 0 g i x = 0) :
ι →₀ N

Given l, a finitely supported function from the sigma type Σ i, αs i to β and an ι-indexed family g of functions from (αs i →₀ β) to γ, split_comp defines a finitely supported function from the index type ι to γ given by composing g i with split l i.

Equations
• l.splitComp g hg = { support := l.splitSupport, toFun := fun (i : ι) => g i (l.split i), mem_support_toFun := }
Instances For
theorem Finsupp.sigma_support {ι : Type u_4} {M : Type u_5} {αs : ιType u_13} [Zero M] (l : (i : ι) × αs i →₀ M) :
l.support = l.splitSupport.sigma fun (i : ι) => (l.split i).support
theorem Finsupp.sigma_sum {ι : Type u_4} {M : Type u_5} {N : Type u_7} {αs : ιType u_13} [Zero M] (l : (i : ι) × αs i →₀ M) [] (f : (i : ι) × αs iMN) :
l.sum f = l.splitSupport.sum fun (i : ι) => (l.split i).sum fun (a : αs i) (b : M) => f i, a b
noncomputable def Finsupp.sigmaFinsuppEquivPiFinsupp {α : Type u_1} {η : Type u_14} [] {ιs : ηType u_15} [Zero α] :
((j : η) × ιs j →₀ α) ((j : η) → ιs j →₀ α)

On a Fintype η, Finsupp.split is an equivalence between (Σ (j : η), ιs j) →₀ α and Π j, (ιs j →₀ α).

This is the Finsupp version of Equiv.Pi_curry.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Finsupp.sigmaFinsuppEquivPiFinsupp_apply {α : Type u_1} {η : Type u_14} [] {ιs : ηType u_15} [Zero α] (f : (j : η) × ιs j →₀ α) (j : η) (i : ιs j) :
(Finsupp.sigmaFinsuppEquivPiFinsupp f j) i = f j, i
noncomputable def Finsupp.sigmaFinsuppAddEquivPiFinsupp {η : Type u_14} [] {α : Type u_16} {ιs : ηType u_17} [] :
((j : η) × ιs j →₀ α) ≃+ ((j : η) → ιs j →₀ α)

On a Fintype η, Finsupp.split is an additive equivalence between (Σ (j : η), ιs j) →₀ α and Π j, (ιs j →₀ α).

This is the AddEquiv version of Finsupp.sigmaFinsuppEquivPiFinsupp.

Equations
• Finsupp.sigmaFinsuppAddEquivPiFinsupp = let __src := Finsupp.sigmaFinsuppEquivPiFinsupp; { toEquiv := __src, map_add' := }
Instances For
@[simp]
theorem Finsupp.sigmaFinsuppAddEquivPiFinsupp_apply {η : Type u_14} [] {α : Type u_16} {ιs : ηType u_17} [] (f : (j : η) × ιs j →₀ α) (j : η) (i : ιs j) :
(Finsupp.sigmaFinsuppAddEquivPiFinsupp f j) i = f j, i