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

• 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

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.notMem_graph_snd_zero {α : Type u_1} {M : Type u_5} [Zero M] (a : α) (f : α →₀ M) : (a, 0) ∉ f.graph

@[deprecated Finsupp.notMem_graph_snd_zero (since := "2025-05-23")]

theorem Finsupp.not_mem_graph_snd_zero {α : Type u_1} {M : Type u_5} [Zero M] (a : α) (f : α →₀ M) : (a, 0) ∉ f.graph

Alias of Finsupp.notMem_graph_snd_zero.

@[simp]

theorem Finsupp.image_fst_graph {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] (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 graph

@[simp]

theorem Finsupp.graph_inj {α : Type u_1} {M : Type u_5} [Zero M] {f g : α →₀ M} : f.graph = g.graph ↔ f = g

@[simp]

theorem Finsupp.graph_zero {α : Type u_1} {M : Type u_5} [Zero M] : graph 0 = ∅

@[simp]

theorem Finsupp.graph_eq_empty {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} : f.graph = ∅ ↔ f = 0

Declarations about mapRange

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

• Finsupp.mapRange.equiv f hf hf' = { toFun := Finsupp.mapRange (⇑f) hf, invFun := Finsupp.mapRange (⇑f.symm) hf', left_inv := ⋯, right_inv := ⋯ }

@[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) : (equiv f hf hf') g = mapRange (⇑f) hf g

@[simp]

theorem Finsupp.mapRange.equiv_refl {α : Type u_1} {M : Type u_5} [Zero M] : equiv (Equiv.refl M) ⋯ ⋯ = Equiv.refl (α →₀ 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) : equiv (f.trans f₂) ⋯ ⋯ = (equiv f hf hf').trans (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) : (equiv f hf hf').symm = equiv f.symm hf' hf

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

• Finsupp.mapRange.zeroHom f = { toFun := Finsupp.mapRange ⇑f ⋯, map_zero' := ⋯ }

@[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) : (zeroHom f) g = mapRange ⇑f ⋯ g

@[simp]

theorem Finsupp.mapRange.zeroHom_id {α : Type u_1} {M : Type u_5} [Zero M] : zeroHom (ZeroHom.id M) = ZeroHom.id (α →₀ 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) : zeroHom (f.comp f₂) = (zeroHom f).comp (zeroHom f₂)

def Finsupp.mapRange.addMonoidHom {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] (f : M →+ N) : (α →₀ M) →+ α →₀ N

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

Equations

• Finsupp.mapRange.addMonoidHom f = { toFun := Finsupp.mapRange ⇑f ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Finsupp.mapRange.addMonoidHom_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] (f : M →+ N) (g : α →₀ M) : (addMonoidHom f) g = mapRange ⇑f ⋯ g

@[simp]

theorem Finsupp.mapRange.addMonoidHom_id {α : Type u_1} {M : Type u_5} [AddCommMonoid M] : addMonoidHom (AddMonoidHom.id M) = AddMonoidHom.id (α →₀ M)

theorem Finsupp.mapRange.addMonoidHom_comp {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] (f : N →+ P) (f₂ : M →+ N) : addMonoidHom (f.comp f₂) = (addMonoidHom f).comp (addMonoidHom f₂)

@[simp]

theorem Finsupp.mapRange.addMonoidHom_toZeroHom {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] (f : M →+ N) : ↑(addMonoidHom f) = zeroHom ↑f

theorem Finsupp.mapRange_multiset_sum {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] {F : Type u_13} [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (m : Multiset (α →₀ M)) : mapRange ⇑f ⋯ m.sum = (Multiset.map (fun (x : α →₀ M) => mapRange ⇑f ⋯ x) m).sum

theorem Finsupp.mapRange_finset_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] {F : Type u_13} [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (s : Finset ι) (g : ι → α →₀ M) : mapRange ⇑f ⋯ (∑ x ∈ s, g x) = ∑ x ∈ s, mapRange ⇑f ⋯ (g x)

def Finsupp.mapRange.addEquiv {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] (f : M ≃+ N) : (α →₀ M) ≃+ (α →₀ N)

Finsupp.mapRange.AddMonoidHom as an equiv.

Equations

• Finsupp.mapRange.addEquiv f = { toFun := Finsupp.mapRange ⇑f ⋯, invFun := Finsupp.mapRange ⇑f.symm ⋯, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem Finsupp.mapRange.addEquiv_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] (f : M ≃+ N) (g : α →₀ M) : (addEquiv f) g = mapRange ⇑f ⋯ g

@[simp]

theorem Finsupp.mapRange.addEquiv_refl {α : Type u_1} {M : Type u_5} [AddCommMonoid M] : addEquiv (AddEquiv.refl M) = AddEquiv.refl (α →₀ M)

theorem Finsupp.mapRange.addEquiv_trans {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] (f : M ≃+ N) (f₂ : N ≃+ P) : addEquiv (f.trans f₂) = (addEquiv f).trans (addEquiv f₂)

@[simp]

theorem Finsupp.mapRange.addEquiv_symm {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] (f : M ≃+ N) : (addEquiv f).symm = addEquiv f.symm

@[simp]

theorem Finsupp.mapRange.addEquiv_toAddMonoidHom {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] (f : M ≃+ N) : ↑(addEquiv f) = addMonoidHom f.toAddMonoidHom

@[simp]

theorem Finsupp.mapRange.addEquiv_toEquiv {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] (f : M ≃+ N) : ↑(addEquiv f) = equiv ↑f ⋯ ⋯

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

• Finsupp.equivMapDomain f l = { support := Finset.map f.toEmbedding l.support, toFun := fun (a : β) => l (f.symm a), mem_support_toFun := ⋯ }

@[simp]

theorem Finsupp.equivMapDomain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α ≃ β) (l : α →₀ M) (b : β) : (equivMapDomain f l) 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 : α) : (equivMapDomain f.symm l) a = l (f a)

@[simp]

theorem Finsupp.equivMapDomain_refl {α : Type u_1} {M : Type u_5} [Zero M] (l : α →₀ M) : equivMapDomain (Equiv.refl α) l = l

theorem Finsupp.equivMapDomain_refl' {α : Type u_1} {M : Type u_5} [Zero M] : equivMapDomain (Equiv.refl α) = id

theorem Finsupp.equivMapDomain_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [Zero M] (f : α ≃ β) (g : β ≃ γ) (l : α →₀ M) : equivMapDomain (f.trans g) l = equivMapDomain g (equivMapDomain f l)

theorem Finsupp.equivMapDomain_trans' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [Zero M] (f : α ≃ β) (g : β ≃ γ) : equivMapDomain (f.trans g) = equivMapDomain g ∘ equivMapDomain f

@[simp]

theorem Finsupp.equivMapDomain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α ≃ β) (a : α) (b : M) : equivMapDomain f (single a b) = single (f a) b

@[simp]

theorem Finsupp.equivMapDomain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : α ≃ β} : equivMapDomain f 0 = 0

@[simp]

theorem Finsupp.prod_equivMapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [Zero M] [CommMonoid N] (f : α ≃ β) (l : α →₀ M) (g : β → M → N) : (equivMapDomain f l).prod g = l.prod fun (a : α) (m : M) => g (f a) m

@[simp]

theorem Finsupp.sum_equivMapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [Zero M] [AddCommMonoid N] (f : α ≃ β) (l : α →₀ M) (g : β → M → N) : (equivMapDomain f l).sum g = l.sum 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

• Finsupp.equivCongrLeft f = { toFun := Finsupp.equivMapDomain f, invFun := Finsupp.equivMapDomain f.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Finsupp.equivCongrLeft_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α ≃ β) (l : α →₀ M) : (equivCongrLeft f) l = equivMapDomain f l

@[simp]

theorem Finsupp.equivCongrLeft_symm {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α ≃ β) : (equivCongrLeft f).symm = equivCongrLeft f.symm

@[simp]

theorem Nat.cast_finsuppProd {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [CommSemiring R] (g : α → M → ℕ) : ↑(f.prod g) = f.prod fun (a : α) (b : M) => ↑(g a b)

@[deprecated Nat.cast_finsuppProd (since := "2025-04-06")]

theorem Nat.cast_finsupp_prod {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [CommSemiring R] (g : α → M → ℕ) : ↑(f.prod g) = f.prod fun (a : α) (b : M) => ↑(g a b)

Alias of Nat.cast_finsuppProd.

@[simp]

theorem Nat.cast_finsupp_sum {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [AddCommMonoidWithOne R] (g : α → M → ℕ) : ↑(f.sum g) = f.sum fun (a : α) (b : M) => ↑(g a b)

@[simp]

theorem Int.cast_finsuppProd {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [CommRing R] (g : α → M → ℤ) : ↑(f.prod g) = f.prod fun (a : α) (b : M) => ↑(g a b)

@[deprecated Int.cast_finsuppProd (since := "2025-04-06")]

theorem Int.cast_finsupp_prod {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [CommRing R] (g : α → M → ℤ) : ↑(f.prod g) = f.prod fun (a : α) (b : M) => ↑(g a b)

Alias of Int.cast_finsuppProd.

@[simp]

theorem Int.cast_finsupp_sum {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [AddCommGroupWithOne R] (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) [DivisionRing R] [CharZero R] (g : α → M → ℚ) : ↑(f.sum g) = f.sum fun (a : α) (b : M) => ↑(g a b)

@[simp]

theorem Rat.cast_finsuppProd {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [Field R] [CharZero R] (g : α → M → ℚ) : ↑(f.prod g) = f.prod fun (a : α) (b : M) => ↑(g a b)

@[deprecated Rat.cast_finsuppProd (since := "2025-04-06")]

theorem Rat.cast_finsupp_prod {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [Field R] [CharZero R] (g : α → M → ℚ) : ↑(f.prod g) = f.prod fun (a : α) (b : M) => ↑(g a b)

Alias of Rat.cast_finsuppProd.

Declarations about mapDomain

def Finsupp.mapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (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

• Finsupp.mapDomain f v = v.sum fun (a : α) => Finsupp.single (f a)

theorem Finsupp.mapDomain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {f : α → β} (hf : Function.Injective f) (x : α →₀ M) (a : α) : (mapDomain f x) (f a) = x a

theorem Finsupp.mapDomain_notin_range {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {f : α → β} (x : α →₀ M) (a : β) (h : a ∉ Set.range f) : (mapDomain f x) a = 0

@[simp]

theorem Finsupp.mapDomain_id {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {v : α →₀ M} : mapDomain id v = v

theorem Finsupp.mapDomain_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [AddCommMonoid M] {v : α →₀ M} {f : α → β} {g : β → γ} : mapDomain (g ∘ f) v = mapDomain g (mapDomain f v)

@[simp]

theorem Finsupp.mapDomain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {f : α → β} {a : α} {b : M} : mapDomain f (single a b) = single (f a) b

@[simp]

theorem Finsupp.mapDomain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {f : α → β} : mapDomain f 0 = 0

theorem Finsupp.mapDomain_congr {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {v : α →₀ M} {f g : α → β} (h : ∀ x ∈ v.support, f x = g x) : mapDomain f v = mapDomain g v

theorem Finsupp.mapDomain_add {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {v₁ v₂ : α →₀ M} {f : α → β} : mapDomain f (v₁ + v₂) = mapDomain f v₁ + mapDomain f v₂

@[simp]

theorem Finsupp.mapDomain_equiv_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {f : α ≃ β} (x : α →₀ M) (a : β) : (mapDomain (⇑f) x) a = x (f.symm a)

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

Finsupp.mapDomain is an AddMonoidHom.

Equations

• Finsupp.mapDomain.addMonoidHom f = { toFun := Finsupp.mapDomain f, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

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

@[simp]

theorem Finsupp.mapDomain.addMonoidHom_id {α : Type u_1} {M : Type u_5} [AddCommMonoid M] : addMonoidHom id = AddMonoidHom.id (α →₀ M)

theorem Finsupp.mapDomain.addMonoidHom_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [AddCommMonoid M] (f : β → γ) (g : α → β) : addMonoidHom (f ∘ g) = (addMonoidHom f).comp (addMonoidHom g)

theorem Finsupp.mapDomain_finset_sum {α : Type u_1} {β : Type u_2} {ι : Type u_4} {M : Type u_5} [AddCommMonoid M] {f : α → β} {s : Finset ι} {v : ι → α →₀ M} : mapDomain f (∑ i ∈ s, v i) = ∑ i ∈ s, mapDomain f (v i)

theorem Finsupp.mapDomain_sum {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [Zero N] {f : α → β} {s : α →₀ N} {v : α → N → α →₀ M} : mapDomain f (s.sum v) = s.sum fun (a : α) (b : N) => mapDomain f (v a b)

theorem Finsupp.mapDomain_support {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] [DecidableEq β] {f : α → β} {s : α →₀ M} : (mapDomain f s).support ⊆ Finset.image f s.support

theorem Finsupp.mapDomain_apply' {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (S : Set α) {f : α → β} (x : α →₀ M) (hS : ↑x.support ⊆ S) (hf : Set.InjOn f S) {a : α} (ha : a ∈ S) : (mapDomain f x) (f a) = x a

theorem Finsupp.mapDomain_support_of_injOn {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] [DecidableEq β] {f : α → β} (s : α →₀ M) (hf : Set.InjOn f ↑s.support) : (mapDomain f s).support = Finset.image f s.support

theorem Finsupp.mapDomain_support_of_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] [DecidableEq β] {f : α → β} (hf : Function.Injective f) (s : α →₀ M) : (mapDomain f s).support = Finset.image f s.support

theorem Finsupp.prod_mapDomain_index {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [CommMonoid N] {f : α → β} {s : α →₀ M} {h : β → M → N} (h_zero : ∀ (b : β), h b 0 = 1) (h_add : ∀ (b : β) (m₁ m₂ : M), h b (m₁ + m₂) = h b m₁ * h b m₂) : (mapDomain f s).prod h = s.prod fun (a : α) (m : M) => h (f a) m

theorem Finsupp.sum_mapDomain_index {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] {f : α → β} {s : α →₀ M} {h : β → M → N} (h_zero : ∀ (b : β), h b 0 = 0) (h_add : ∀ (b : β) (m₁ m₂ : M), h b (m₁ + m₂) = h b m₁ + h b m₂) : (mapDomain f s).sum h = s.sum 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} [AddCommMonoid M] [AddCommMonoid N] {f : α → β} {s : α →₀ M} (h : β → M →+ N) : ((mapDomain f s).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} [AddCommMonoid M] (f : α ↪ β) (v : α →₀ M) : embDomain f v = mapDomain (⇑f) v

theorem Finsupp.prod_mapDomain_index_inj {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [CommMonoid N] {f : α → β} {s : α →₀ M} {h : β → M → N} (hf : Function.Injective f) : (mapDomain f s).prod h = s.prod fun (a : α) (b : M) => h (f a) b

theorem Finsupp.sum_mapDomain_index_inj {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] {f : α → β} {s : α →₀ M} {h : β → M → N} (hf : Function.Injective f) : (mapDomain f s).sum h = s.sum fun (a : α) (b : M) => h (f a) b

theorem Finsupp.mapDomain_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {f : α → β} (hf : Function.Injective f) : Function.Injective (mapDomain f)

theorem Finsupp.mapDomain_surjective {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {f : α → β} (hf : Function.Surjective f) : Function.Surjective (mapDomain f)

def Finsupp.mapDomainEmbedding {α : Type u_13} {β : Type u_14} (f : α ↪ β) : (α →₀ ℕ) ↪ β →₀ ℕ

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

Equations

• Finsupp.mapDomainEmbedding f = { toFun := Finsupp.mapDomain ⇑f, inj' := ⋯ }

@[simp]

theorem Finsupp.mapDomainEmbedding_apply {α : Type u_13} {β : Type u_14} (f : α ↪ β) (v : α →₀ ℕ) : (mapDomainEmbedding f) v = mapDomain (⇑f) v

theorem Finsupp.mapDomain.addMonoidHom_comp_mapRange {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] (f : α → β) (g : M →+ N) : (addMonoidHom f).comp (mapRange.addMonoidHom g) = (mapRange.addMonoidHom g).comp (addMonoidHom f)

theorem Finsupp.mapDomain_mapRange {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] (f : α → β) (v : α →₀ M) (g : M → N) (h0 : g 0 = 0) (hadd : ∀ (x y : M), g (x + y) = g x + g y) : mapDomain f (mapRange g h0 v) = mapRange g h0 (mapDomain f v)

When g preserves addition, mapRange and mapDomain commute.

theorem Finsupp.sum_update_add {α : Type u_1} {β : Type u_2} {ι : Type u_4} [AddZeroClass α] [AddCommMonoid β] (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} [AddCommMonoid M] (S : Set α) {f : α → β} (hf : Set.InjOn f S) : Set.InjOn (mapDomain f) {w : α →₀ M | ↑w.support ⊆ S}

theorem Finsupp.equivMapDomain_eq_mapDomain {α : Type u_1} {β : Type u_2} {M : Type u_13} [AddCommMonoid M] (f : α ≃ β) (l : α →₀ M) : equivMapDomain f l = mapDomain (⇑f) l

Declarations about comapDomain

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

• Finsupp.comapDomain f l hf = { support := l.support.preimage f hf, toFun := fun (a : α) => l (f a), mem_support_toFun := ⋯ }

@[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)) : (comapDomain f l hf).support = l.support.preimage f hf

@[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 : α) : (comapDomain f l hf) a = l (f a)

theorem Finsupp.sum_comapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [Zero M] [AddCommMonoid N] (f : α → β) (l : β →₀ M) (g : β → M → N) (hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support) : (comapDomain f l ⋯).sum (g ∘ f) = l.sum g

theorem Finsupp.eq_zero_of_comapDomain_eq_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α → β) (l : β →₀ M) (hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support) : comapDomain f l ⋯ = 0 → l = 0

theorem Finsupp.embDomain_comapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : α ↪ β} {g : β →₀ M} (hg : ↑g.support ⊆ Set.range ⇑f) : embDomain f (comapDomain (⇑f) g ⋯) = g

@[simp]

theorem Finsupp.comapDomain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α → β) (hif : Set.InjOn f (f ⁻¹' ↑(support 0)) := ⋯) : comapDomain f 0 hif = 0

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 ⁻¹' ↑(single (f a) m).support)) : comapDomain f (single (f a) m) hif = single a m

theorem Finsupp.comapDomain_add {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] {f : α → β} (v₁ v₂ : β →₀ M) (hv₁ : Set.InjOn f (f ⁻¹' ↑v₁.support)) (hv₂ : Set.InjOn f (f ⁻¹' ↑v₂.support)) (hv₁₂ : Set.InjOn f (f ⁻¹' ↑(v₁ + v₂).support)) : comapDomain f (v₁ + v₂) hv₁₂ = comapDomain f v₁ hv₁ + comapDomain f v₂ hv₂

theorem Finsupp.comapDomain_add_of_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] {f : α → β} (hf : Function.Injective f) (v₁ v₂ : β →₀ M) : comapDomain f (v₁ + v₂) ⋯ = comapDomain f v₁ ⋯ + comapDomain f v₂ ⋯

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

def Finsupp.comapDomain.addMonoidHom {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] {f : α → β} (hf : Function.Injective f) : (β →₀ M) →+ α →₀ M

Finsupp.comapDomain is an AddMonoidHom.

Equations

• Finsupp.comapDomain.addMonoidHom hf = { toFun := fun (x : β →₀ M) => Finsupp.comapDomain f x ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Finsupp.comapDomain.addMonoidHom_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] {f : α → β} (hf : Function.Injective f) (x : β →₀ M) : (addMonoidHom hf) x = comapDomain f x ⋯

theorem Finsupp.mapDomain_comapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (f : α → β) (hf : Function.Injective f) (l : β →₀ M) (hl : ↑l.support ⊆ Set.range f) : mapDomain f (comapDomain f l ⋯) = l

theorem Finsupp.comapDomain_mapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (f : α → β) (hf : Function.Injective f) (l : α →₀ M) : comapDomain f (mapDomain f l) ⋯ = l

Declarations about Finsupp.filter

def Finsupp.filter {α : Type u_1} {M : Type u_5} [Zero M] (p : α → Prop) [DecidablePred p] (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

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

theorem Finsupp.filter_apply {α : Type u_1} {M : Type u_5} [Zero M] (p : α → Prop) [DecidablePred p] (f : α →₀ M) (a : α) : (filter p f) 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) [DecidablePred p] (f : α →₀ M) : ⇑(filter p f) = {x : α | p x}.indicator ⇑f

theorem Finsupp.filter_eq_zero_iff {α : Type u_1} {M : Type u_5} [Zero M] (p : α → Prop) [DecidablePred p] (f : α →₀ M) : filter p f = 0 ↔ ∀ (x : α), p x → f x = 0

theorem Finsupp.filter_eq_self_iff {α : Type u_1} {M : Type u_5} [Zero M] (p : α → Prop) [DecidablePred p] (f : α →₀ M) : filter p f = f ↔ ∀ (x : α), f x ≠ 0 → p x

@[simp]

theorem Finsupp.filter_apply_pos {α : Type u_1} {M : Type u_5} [Zero M] (p : α → Prop) [DecidablePred p] (f : α →₀ M) {a : α} (h : p a) : (filter p f) a = f a

@[simp]

theorem Finsupp.filter_apply_neg {α : Type u_1} {M : Type u_5} [Zero M] (p : α → Prop) [DecidablePred p] (f : α →₀ M) {a : α} (h : ¬p a) : (filter p f) a = 0

@[simp]

theorem Finsupp.support_filter {α : Type u_1} {M : Type u_5} [Zero M] (p : α → Prop) [DecidablePred p] (f : α →₀ M) : (filter p f).support = {x ∈ f.support | p x}

theorem Finsupp.filter_zero {α : Type u_1} {M : Type u_5} [Zero M] (p : α → Prop) [DecidablePred p] : filter p 0 = 0

@[simp]

theorem Finsupp.filter_single_of_pos {α : Type u_1} {M : Type u_5} [Zero M] (p : α → Prop) [DecidablePred p] {a : α} {b : M} (h : p a) : filter p (single a b) = single a b

@[simp]

theorem Finsupp.filter_single_of_neg {α : Type u_1} {M : Type u_5} [Zero M] (p : α → Prop) [DecidablePred p] {a : α} {b : M} (h : ¬p a) : filter p (single a b) = 0

theorem Finsupp.prod_filter_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] (p : α → Prop) [DecidablePred p] (f : α →₀ M) [CommMonoid N] (g : α → M → N) : (filter p f).prod g = ∏ x ∈ (filter p f).support, g x (f x)

theorem Finsupp.sum_filter_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] (p : α → Prop) [DecidablePred p] (f : α →₀ M) [AddCommMonoid N] (g : α → M → N) : (filter p f).sum g = ∑ x ∈ (filter p f).support, g x (f x)

@[simp]

theorem Finsupp.prod_filter_mul_prod_filter_not {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] (p : α → Prop) [DecidablePred p] (f : α →₀ M) [CommMonoid N] (g : α → M → N) : (filter p f).prod g * (filter (fun (a : α) => ¬p a) f).prod g = f.prod g

@[simp]

theorem Finsupp.sum_filter_add_sum_filter_not {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] (p : α → Prop) [DecidablePred p] (f : α →₀ M) [AddCommMonoid N] (g : α → M → N) : (filter p f).sum g + (filter (fun (a : α) => ¬p a) f).sum g = 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) [DecidablePred p] (f : α →₀ M) [CommGroup G] (g : α → M → G) : f.prod g / (filter p f).prod g = (filter (fun (a : α) => ¬p a) 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) [DecidablePred p] (f : α →₀ M) [AddCommGroup G] (g : α → M → G) : f.sum g - (filter p f).sum g = (filter (fun (a : α) => ¬p a) f).sum g

theorem Finsupp.filter_pos_add_filter_neg {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f : α →₀ M) (p : α → Prop) [DecidablePred p] : filter p f + filter (fun (a : α) => ¬p a) f = f

Declarations about frange

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

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

Equations

• f.frange = Finset.image (⇑f) f.support

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_notMem_frange {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} : 0 ∉ f.frange

@[deprecated Finsupp.zero_notMem_frange (since := "2025-05-23")]

theorem Finsupp.zero_not_mem_frange {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} : 0 ∉ f.frange

Alias of Finsupp.zero_notMem_frange.

theorem Finsupp.frange_single {α : Type u_1} {M : Type u_5} [Zero M] {x : α} {y : M} : (single x y).frange ⊆ {y}

Declarations about Finsupp.subtypeDomain

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

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

Equations

• Finsupp.subtypeDomain p f = { support := Finset.subtype p f.support, toFun := ⇑f ∘ Subtype.val, mem_support_toFun := ⋯ }

@[simp]

theorem Finsupp.support_subtypeDomain {α : Type u_1} {M : Type u_5} [Zero M] {p : α → Prop} [D : DecidablePred p] {f : α →₀ M} : (subtypeDomain p f).support = Finset.subtype p f.support

@[simp]

theorem Finsupp.subtypeDomain_apply {α : Type u_1} {M : Type u_5} [Zero M] {p : α → Prop} {a : Subtype p} {v : α →₀ M} : (subtypeDomain p v) a = v ↑a

@[simp]

theorem Finsupp.subtypeDomain_zero {α : Type u_1} {M : Type u_5} [Zero M] {p : α → Prop} : subtypeDomain p 0 = 0

theorem Finsupp.subtypeDomain_eq_iff_forall {α : Type u_1} {M : Type u_5} [Zero M] {p : α → Prop} {f g : α →₀ M} : subtypeDomain p f = subtypeDomain p g ↔ ∀ (x : α), p x → f x = g x

theorem Finsupp.subtypeDomain_eq_iff {α : Type u_1} {M : Type u_5} [Zero M] {p : α → Prop} {f g : α →₀ M} (hf : ∀ x ∈ f.support, p x) (hg : ∀ x ∈ g.support, p x) : subtypeDomain p f = subtypeDomain p g ↔ f = g

theorem Finsupp.subtypeDomain_eq_zero_iff' {α : Type u_1} {M : Type u_5} [Zero M] {p : α → Prop} {f : α →₀ M} : subtypeDomain p f = 0 ↔ ∀ (x : α), p x → f x = 0

theorem Finsupp.subtypeDomain_eq_zero_iff {α : Type u_1} {M : Type u_5} [Zero M] {p : α → Prop} {f : α →₀ M} (hf : ∀ x ∈ f.support, p x) : subtypeDomain p f = 0 ↔ f = 0

theorem Finsupp.prod_subtypeDomain_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] {p : α → Prop} [CommMonoid N] {v : α →₀ M} {h : α → M → N} (hp : ∀ x ∈ v.support, p x) : ((subtypeDomain p v).prod fun (a : Subtype p) (b : M) => h (↑a) b) = v.prod h

theorem Finsupp.sum_subtypeDomain_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] {p : α → Prop} [AddCommMonoid N] {v : α →₀ M} {h : α → M → N} (hp : ∀ x ∈ v.support, p x) : ((subtypeDomain p v).sum fun (a : Subtype p) (b : M) => h (↑a) b) = v.sum h

@[simp]

theorem Finsupp.subtypeDomain_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] {p : α → Prop} {v v' : α →₀ M} : subtypeDomain p (v + v') = subtypeDomain p v + subtypeDomain p v'

def Finsupp.subtypeDomainAddMonoidHom {α : Type u_1} {M : Type u_5} [AddZeroClass M] {p : α → Prop} : (α →₀ M) →+ Subtype p →₀ M

subtypeDomain but as an AddMonoidHom.

Equations

• Finsupp.subtypeDomainAddMonoidHom = { toFun := Finsupp.subtypeDomain p, map_zero' := ⋯, map_add' := ⋯ }

def Finsupp.filterAddHom {α : Type u_1} {M : Type u_5} [AddZeroClass M] (p : α → Prop) [DecidablePred p] : (α →₀ M) →+ α →₀ M

Finsupp.filter as an AddMonoidHom.

Equations

• Finsupp.filterAddHom p = { toFun := Finsupp.filter p, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Finsupp.filter_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] {p : α → Prop} [DecidablePred p] {v v' : α →₀ M} : filter p (v + v') = filter p v + filter p v'

theorem Finsupp.subtypeDomain_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} [AddCommMonoid M] {p : α → Prop} {s : Finset ι} {h : ι → α →₀ M} : subtypeDomain p (∑ c ∈ s, h c) = ∑ c ∈ s, subtypeDomain p (h c)

theorem Finsupp.subtypeDomain_finsupp_sum {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] {p : α → Prop} [Zero N] {s : β →₀ N} {h : β → N → α →₀ M} : subtypeDomain p (s.sum h) = s.sum fun (c : β) (d : N) => subtypeDomain p (h c d)

theorem Finsupp.filter_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} [AddCommMonoid M] {p : α → Prop} [DecidablePred p] (s : Finset ι) (f : ι → α →₀ M) : filter p (∑ a ∈ s, f a) = ∑ a ∈ s, filter p (f a)

theorem Finsupp.filter_eq_sum {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (p : α → Prop) [DecidablePred p] (f : α →₀ M) : filter p f = ∑ i ∈ f.support with p i, single i (f i)

@[simp]

theorem Finsupp.subtypeDomain_neg {α : Type u_1} {G : Type u_9} [AddGroup G] {p : α → Prop} {v : α →₀ G} : subtypeDomain p (-v) = -subtypeDomain p v

@[simp]

theorem Finsupp.subtypeDomain_sub {α : Type u_1} {G : Type u_9} [AddGroup G] {p : α → Prop} {v v' : α →₀ G} : subtypeDomain p (v - v') = subtypeDomain p v - subtypeDomain p v'

@[simp]

theorem Finsupp.filter_neg {α : Type u_1} {G : Type u_9} [AddGroup G] (p : α → Prop) [DecidablePred p] (f : α →₀ G) : filter p (-f) = -filter p f

@[simp]

theorem Finsupp.filter_sub {α : Type u_1} {G : Type u_9} [AddGroup G] (p : α → Prop) [DecidablePred p] (f₁ f₂ : α →₀ G) : filter p (f₁ - f₂) = filter p f₁ - filter p f₂

theorem Finsupp.mem_support_multiset_sum {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {s : Multiset (α →₀ M)} (a : α) : a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support

theorem Finsupp.mem_support_finset_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} [AddCommMonoid M] {s : Finset ι} {h : ι → α →₀ M} (a : α) (ha : a ∈ (∑ c ∈ s, h c).support) : ∃ c ∈ s, a ∈ (h c).support

Declarations about curry and uncurry

def Finsupp.uncurry {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (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 = { support := f.support.disjiUnion (fun (a : α) => Finset.map (Function.Embedding.sectR a β) (f a).support) ⋯, toFun := fun (x : α × β) => (f x.1) x.2, mem_support_toFun := ⋯ }

theorem Finsupp.uncurry_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α →₀ β →₀ M) (x : α × β) : f.uncurry x = (f x.1) x.2

@[simp]

theorem Finsupp.uncurry_apply_pair {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α →₀ β →₀ M) (a : α) (b : β) : f.uncurry (a, b) = (f a) b

@[simp]

theorem Finsupp.uncurry_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (a : α) (b : β) (m : M) : (single a (single b m)).uncurry = single (a, b) m

theorem Finsupp.sum_uncurry_index {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [Zero M] [AddCommMonoid N] (f : α →₀ β →₀ M) (g : α × β → M → N) : (f.uncurry.sum fun (p : α × β) (c : M) => g p c) = f.sum fun (a : α) (f : β →₀ M) => f.sum fun (b : β) => g (a, b)

theorem Finsupp.sum_uncurry_index' {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [Zero M] [AddCommMonoid N] (f : α →₀ β →₀ M) (g : α → β → M → N) : (f.uncurry.sum fun (p : α × β) (c : M) => g p.1 p.2 c) = f.sum fun (a : α) (f : β →₀ M) => f.sum (g a)

def Finsupp.curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [DecidableEq α] [Zero M] (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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finsupp.curry_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [DecidableEq α] [Zero M] (f : α × β →₀ M) (x : α) (y : β) : (f.curry x) y = f (x, y)

@[simp]

theorem Finsupp.support_curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [DecidableEq α] [Zero M] (f : α × β →₀ M) : f.curry.support = Finset.image Prod.fst f.support

@[simp]

theorem Finsupp.curry_uncurry {α : Type u_1} {β : Type u_2} {M : Type u_5} [DecidableEq α] [Zero M] (f : α →₀ β →₀ M) : f.uncurry.curry = f

@[simp]

theorem Finsupp.uncurry_curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [DecidableEq α] [Zero M] (f : α × β →₀ M) : f.curry.uncurry = f

@[simp]

theorem Finsupp.curry_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [DecidableEq α] [Zero M] (a : α × β) (m : M) : (single a m).curry = single a.1 (single a.2 m)

theorem Finsupp.sum_curry_index {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [DecidableEq α] [Zero M] [AddCommMonoid N] (f : α × β →₀ M) (g : α → β → M → N) : (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.finsuppProdEquiv {α : Type u_1} {β : Type u_2} {M : Type u_5} [DecidableEq α] [Zero M] : (α × β →₀ 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 := ⋯ }

@[simp]

theorem Finsupp.finsuppProdEquiv_symm_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [DecidableEq α] [Zero M] (f : α →₀ β →₀ M) : finsuppProdEquiv.symm f = f.uncurry

@[simp]

theorem Finsupp.finsuppProdEquiv_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [DecidableEq α] [Zero M] (f : α × β →₀ M) : finsuppProdEquiv f = f.curry

theorem Finsupp.filter_curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [DecidableEq α] [Zero M] (f : α × β →₀ M) (p : α → Prop) [DecidablePred p] : (filter (fun (a : α × β) => p a.1) f).curry = filter p f.curry

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

• f.sumElim g = { support := f.support.disjSum g.support, toFun := Sum.elim ⇑f ⇑g, mem_support_toFun := ⋯ }

@[simp]

theorem Finsupp.sumElim_support {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α →₀ γ) (g : β →₀ γ) : (f.sumElim g).support = f.support.disjSum g.support

@[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) (Sum.inl x) = f x

theorem Finsupp.sumElim_inr {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α →₀ γ) (g : β →₀ γ) (x : β) : (f.sumElim g) (Sum.inr x) = g x

theorem Finsupp.prod_sumElim {ι₁ : Type u_13} {ι₂ : Type u_14} {α : Type u_15} {M : Type u_16} [Zero α] [CommMonoid M] (f₁ : ι₁ →₀ α) (f₂ : ι₂ →₀ α) (g : ι₁ ⊕ ι₂ → α → M) : (f₁.sumElim f₂).prod g = f₁.prod (g ∘ Sum.inl) * f₂.prod (g ∘ Sum.inr)

theorem Finsupp.sum_sumElim {ι₁ : Type u_13} {ι₂ : Type u_14} {α : Type u_15} {M : Type u_16} [Zero α] [AddCommMonoid M] (f₁ : ι₁ →₀ α) (f₂ : ι₂ →₀ α) (g : ι₁ ⊕ ι₂ → α → M) : (f₁.sumElim f₂).sum g = f₁.sum (g ∘ Sum.inl) + f₂.sum (g ∘ Sum.inr)

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.

@[simp]

theorem Finsupp.sumFinsuppEquivProdFinsupp_symm_apply {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (fg : (α →₀ γ) × (β →₀ γ)) : sumFinsuppEquivProdFinsupp.symm fg = fg.1.sumElim fg.2

@[simp]

theorem Finsupp.sumFinsuppEquivProdFinsupp_apply {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α ⊕ β →₀ γ) : sumFinsuppEquivProdFinsupp f = (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)

theorem Finsupp.fst_sumFinsuppEquivProdFinsupp {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α ⊕ β →₀ γ) (x : α) : (sumFinsuppEquivProdFinsupp f).1 x = f (Sum.inl x)

theorem Finsupp.snd_sumFinsuppEquivProdFinsupp {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α ⊕ β →₀ γ) (y : β) : (sumFinsuppEquivProdFinsupp f).2 y = f (Sum.inr y)

theorem Finsupp.sumFinsuppEquivProdFinsupp_symm_inl {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (fg : (α →₀ γ) × (β →₀ γ)) (x : α) : (sumFinsuppEquivProdFinsupp.symm fg) (Sum.inl x) = fg.1 x

theorem Finsupp.sumFinsuppEquivProdFinsupp_symm_inr {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (fg : (α →₀ γ) × (β →₀ γ)) (y : β) : (sumFinsuppEquivProdFinsupp.symm fg) (Sum.inr y) = fg.2 y

def Finsupp.sumFinsuppAddEquivProdFinsupp {M : Type u_5} [AddMonoid M] {α : 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 = { toEquiv := Finsupp.sumFinsuppEquivProdFinsupp, map_add' := ⋯ }

@[simp]

theorem Finsupp.sumFinsuppAddEquivProdFinsupp_symm_apply {M : Type u_5} [AddMonoid M] {α : Type u_13} {β : Type u_14} (fg : (α →₀ M) × (β →₀ M)) : sumFinsuppAddEquivProdFinsupp.symm fg = fg.1.sumElim fg.2

@[simp]

theorem Finsupp.sumFinsuppAddEquivProdFinsupp_apply {M : Type u_5} [AddMonoid M] {α : Type u_13} {β : Type u_14} (f : α ⊕ β →₀ M) : sumFinsuppAddEquivProdFinsupp f = (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)

theorem Finsupp.fst_sumFinsuppAddEquivProdFinsupp {M : Type u_5} [AddMonoid M] {α : Type u_13} {β : Type u_14} (f : α ⊕ β →₀ M) (x : α) : (sumFinsuppAddEquivProdFinsupp f).1 x = f (Sum.inl x)

theorem Finsupp.snd_sumFinsuppAddEquivProdFinsupp {M : Type u_5} [AddMonoid M] {α : Type u_13} {β : Type u_14} (f : α ⊕ β →₀ M) (y : β) : (sumFinsuppAddEquivProdFinsupp f).2 y = f (Sum.inr y)

theorem Finsupp.sumFinsuppAddEquivProdFinsupp_symm_inl {M : Type u_5} [AddMonoid M] {α : Type u_13} {β : Type u_14} (fg : (α →₀ M) × (β →₀ M)) (x : α) : (sumFinsuppAddEquivProdFinsupp.symm fg) (Sum.inl x) = fg.1 x

theorem Finsupp.sumFinsuppAddEquivProdFinsupp_symm_inr {M : Type u_5} [AddMonoid M] {α : Type u_13} {β : Type u_14} (fg : (α →₀ M) × (β →₀ M)) (y : β) : (sumFinsuppAddEquivProdFinsupp.symm fg) (Sum.inr y) = fg.2 y

instance Finsupp.uniqueOfRight {α : Type u_1} {R : Type u_11} [Zero R] [Subsingleton 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] [IsEmpty α] : Unique (α →₀ R)

The Finsupp version of Pi.uniqueOfIsEmpty.

Equations

• Finsupp.uniqueOfLeft = ⋯.unique

def Finsupp.piecewise {α : Type u_1} {M : Type u_13} [Zero M] {P : α → Prop} [DecidablePred P] (f : Subtype P →₀ 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.

@[simp]

theorem Finsupp.piecewise_support {α : Type u_1} {M : Type u_13} [Zero M] {P : α → Prop} [DecidablePred P] (f : Subtype P →₀ M) (g : { a : α // ¬P a } →₀ M) : (f.piecewise g).support = (Finset.map (Function.Embedding.subtype P) 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} [DecidablePred P] (f : Subtype P →₀ M) (g : { a : α // ¬P a } →₀ M) (a : α) : (f.piecewise g) a = if h : P a then f ⟨a, h⟩ else g ⟨a, h⟩

@[simp]

theorem Finsupp.subtypeDomain_piecewise {α : Type u_1} {M : Type u_13} [Zero M] {P : α → Prop} [DecidablePred P] (f : Subtype P →₀ M) (g : { a : α // ¬P a } →₀ M) : subtypeDomain P (f.piecewise g) = f

@[simp]

theorem Finsupp.subtypeDomain_not_piecewise {α : Type u_1} {M : Type u_13} [Zero M] {P : α → Prop} [DecidablePred P] (f : Subtype P →₀ M) (g : { a : α // ¬P a } →₀ M) : subtypeDomain (fun (x : α) => ¬P x) (f.piecewise g) = g

def Finsupp.extendDomain {α : Type u_1} {M : Type u_13} [Zero M] {P : α → Prop} [DecidablePred P] (f : Subtype P →₀ M) : α →₀ M

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

Equations

• f.extendDomain = f.piecewise 0

@[simp]

theorem Finsupp.extendDomain_toFun {α : Type u_1} {M : Type u_13} [Zero M] {P : α → Prop} [DecidablePred P] (f : Subtype P →₀ 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} [DecidablePred P] (f : Subtype P →₀ M) : f.extendDomain.support = Finset.map (Function.Embedding.subtype P) f.support

theorem Finsupp.extendDomain_eq_embDomain_subtype {α : Type u_1} {M : Type u_13} [Zero M] {P : α → Prop} [DecidablePred P] (f : Subtype P →₀ M) : f.extendDomain = embDomain (Function.Embedding.subtype P) f

theorem Finsupp.support_extendDomain_subset {α : Type u_1} {M : Type u_13} [Zero M] {P : α → Prop} [DecidablePred P] (f : Subtype P →₀ M) : ↑f.extendDomain.support ⊆ {x : α | P x}

@[simp]

theorem Finsupp.subtypeDomain_extendDomain {α : Type u_1} {M : Type u_13} [Zero M] {P : α → Prop} [DecidablePred P] (f : Subtype P →₀ M) : subtypeDomain P f.extendDomain = f

theorem Finsupp.extendDomain_subtypeDomain {α : Type u_1} {M : Type u_13} [Zero M] {P : α → Prop} [DecidablePred P] (f : α →₀ M) (hf : ∀ a ∈ f.support, P a) : (subtypeDomain P f).extendDomain = f

@[simp]

theorem Finsupp.extendDomain_single {α : Type u_1} {M : Type u_13} [Zero M] {P : α → Prop} [DecidablePred P] (a : Subtype P) (m : M) : (single a m).extendDomain = single (↑a) m

def Finsupp.restrictSupportEquiv {α : Type u_1} (s : Set α) (M : Type u_13) [AddCommMonoid M] : { 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.

@[simp]

theorem Finsupp.restrictSupportEquiv_apply {α : Type u_1} (s : Set α) (M : Type u_13) [AddCommMonoid M] (f : { f : α →₀ M // ↑f.support ⊆ s }) : (restrictSupportEquiv s M) f = subtypeDomain (fun (x : α) => x ∈ s) ↑f

@[simp]

theorem Finsupp.restrictSupportEquiv_symm_apply_coe {α : Type u_1} (s : Set α) (M : Type u_13) [AddCommMonoid M] [DecidablePred fun (x : α) => x ∈ s] (f : ↑s →₀ M) : ↑((restrictSupportEquiv s M).symm f) = f.extendDomain

@[simp]

theorem Finsupp.restrictSupportEquiv_symm_single {α : Type u_1} (s : Set α) (M : Type u_13) [AddCommMonoid M] (a : ↑s) (x : M) : ↑((restrictSupportEquiv s M).symm (single a x)) = single (↑a) x

def Finsupp.domCongr {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (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

• Finsupp.domCongr e = { toFun := Finsupp.equivMapDomain e, invFun := Finsupp.equivMapDomain e.symm, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem Finsupp.domCongr_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (e : α ≃ β) (l : α →₀ M) : (Finsupp.domCongr e) l = equivMapDomain e l

@[simp]

theorem Finsupp.domCongr_refl {α : Type u_1} {M : Type u_5} [AddCommMonoid M] : Finsupp.domCongr (Equiv.refl α) = AddEquiv.refl (α →₀ M)

@[simp]

theorem Finsupp.domCongr_symm {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (e : α ≃ β) : (Finsupp.domCongr e).symm = Finsupp.domCongr e.symm

@[simp]

theorem Finsupp.domCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [AddCommMonoid M] (e : α ≃ β) (f : β ≃ γ) : (Finsupp.domCongr e).trans (Finsupp.domCongr f) = 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 = Finsupp.comapDomain (Sigma.mk i) l ⋯

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) : Finset ι

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

• l.splitSupport = Finset.image Sigma.fst l.support

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

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) [AddCommMonoid N] (f : (i : ι) × αs i → M → N) : l.sum f = ∑ i ∈ l.splitSupport, (l.split i).sum fun (a : αs i) (b : M) => f ⟨i, a⟩ b

noncomputable def Finsupp.sigmaFinsuppEquivPiFinsupp {α : Type u_1} {η : Type u_14} [Fintype η] {ι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.

@[simp]

theorem Finsupp.sigmaFinsuppEquivPiFinsupp_apply {α : Type u_1} {η : Type u_14} [Fintype η] {ιs : η → Type u_15} [Zero α] (f : (j : η) × ιs j →₀ α) (j : η) (i : ιs j) : (sigmaFinsuppEquivPiFinsupp f j) i = f ⟨j, i⟩

noncomputable def Finsupp.sigmaFinsuppAddEquivPiFinsupp {η : Type u_14} [Fintype η] {α : Type u_16} {ιs : η → Type u_17} [AddMonoid α] : ((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 = { toEquiv := Finsupp.sigmaFinsuppEquivPiFinsupp, map_add' := ⋯ }

@[simp]

theorem Finsupp.sigmaFinsuppAddEquivPiFinsupp_apply {η : Type u_14} [Fintype η] {α : Type u_16} {ιs : η → Type u_17} [AddMonoid α] (f : (j : η) × ιs j →₀ α) (j : η) (i : ιs j) : (sigmaFinsuppAddEquivPiFinsupp f j) i = f ⟨j, i⟩