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

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

@[simp]

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

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

@[simp]

theorem Finsupp.mapRange.zeroHom_id {α : Type u_1} {M : Type u_5} [Zero M] : Finsupp.mapRange.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) : Finsupp.mapRange.zeroHom (f.comp f₂) = (Finsupp.mapRange.zeroHom f).comp (Finsupp.mapRange.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) : (Finsupp.mapRange.addMonoidHom f) g = Finsupp.mapRange ⇑f ⋯ g

@[simp]

theorem Finsupp.mapRange.addMonoidHom_id {α : Type u_1} {M : Type u_5} [AddCommMonoid M] : Finsupp.mapRange.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) : Finsupp.mapRange.addMonoidHom (f.comp f₂) = (Finsupp.mapRange.addMonoidHom f).comp (Finsupp.mapRange.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) : ↑(Finsupp.mapRange.addMonoidHom f) = Finsupp.mapRange.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)) : 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} [AddCommMonoid M] [AddCommMonoid N] {F : Type u_13} [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (s : Finset ι) (g : ι → α →₀ M) : Finsupp.mapRange ⇑f ⋯ (∑ x ∈ s, g x) = ∑ x ∈ s, Finsupp.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) : (Finsupp.mapRange.addEquiv f) g = Finsupp.mapRange ⇑f ⋯ g

@[simp]

theorem Finsupp.mapRange.addEquiv_refl {α : Type u_1} {M : Type u_5} [AddCommMonoid M] : Finsupp.mapRange.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) : Finsupp.mapRange.addEquiv (f.trans f₂) = (Finsupp.mapRange.addEquiv f).trans (Finsupp.mapRange.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) : (Finsupp.mapRange.addEquiv f).symm = Finsupp.mapRange.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) : ↑(Finsupp.mapRange.addEquiv f) = Finsupp.mapRange.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) : ↑(Finsupp.mapRange.addEquiv f) = Finsupp.mapRange.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 : β) : (Finsupp.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 : α) : (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) : Finsupp.equivMapDomain (Equiv.refl α) l = l

theorem Finsupp.equivMapDomain_refl' {α : Type u_1} {M : Type u_5} [Zero M] : Finsupp.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) : Finsupp.equivMapDomain (f.trans g) l = Finsupp.equivMapDomain g (Finsupp.equivMapDomain f l)

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

@[simp]

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

@[simp]

theorem Finsupp.equivMapDomain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : α ≃ β} : Finsupp.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) : (Finsupp.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) : (Finsupp.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) : (Finsupp.equivCongrLeft f) l = Finsupp.equivMapDomain f l

@[simp]

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

@[simp]

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)

@[simp]

theorem Nat.cast_finsupp_sum {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [CommSemiring R] (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) [CommRing R] (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) [CommRing 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_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)

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 : α) : (Finsupp.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) : (Finsupp.mapDomain f x) a = 0

@[simp]

theorem Finsupp.mapDomain_id {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {v : α →₀ M} : Finsupp.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 : β → γ} : Finsupp.mapDomain (g ∘ f) v = Finsupp.mapDomain g (Finsupp.mapDomain f v)

@[simp]

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

@[simp]

theorem Finsupp.mapDomain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {f : α → β} : Finsupp.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) : Finsupp.mapDomain f v = Finsupp.mapDomain g v

theorem Finsupp.mapDomain_add {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {v₁ v₂ : α →₀ M} {f : α → β} : Finsupp.mapDomain f (v₁ + v₂) = Finsupp.mapDomain f v₁ + Finsupp.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 : β) : (Finsupp.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) : (Finsupp.mapDomain.addMonoidHom f) v = Finsupp.mapDomain f v

@[simp]

theorem Finsupp.mapDomain.addMonoidHom_id {α : Type u_1} {M : Type u_5} [AddCommMonoid M] : Finsupp.mapDomain.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 : α → β) : Finsupp.mapDomain.addMonoidHom (f ∘ g) = (Finsupp.mapDomain.addMonoidHom f).comp (Finsupp.mapDomain.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} : Finsupp.mapDomain f (∑ i ∈ s, v i) = ∑ i ∈ s, Finsupp.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} : 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} [AddCommMonoid M] [DecidableEq β] {f : α → β} {s : α →₀ M} : (Finsupp.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) : (Finsupp.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) : (Finsupp.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) : (Finsupp.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₂) : (Finsupp.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₂) : (Finsupp.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) : ((Finsupp.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) : Finsupp.embDomain f v = Finsupp.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) : (Finsupp.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) : (Finsupp.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 (Finsupp.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 : α →₀ ℕ) : (Finsupp.mapDomainEmbedding f) v = Finsupp.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) : (Finsupp.mapDomain.addMonoidHom f).comp (Finsupp.mapRange.addMonoidHom g) = (Finsupp.mapRange.addMonoidHom g).comp (Finsupp.mapDomain.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) : Finsupp.mapDomain f (Finsupp.mapRange g h0 v) = Finsupp.mapRange g h0 (Finsupp.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} [AddCommMonoid α] [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 (Finsupp.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) : Finsupp.equivMapDomain f l = Finsupp.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)) : (Finsupp.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 : α) : (Finsupp.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) : (Finsupp.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} [AddCommMonoid M] (f : α → β) (l : β →₀ M) (hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support) : Finsupp.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) : Finsupp.embDomain f (Finsupp.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 ⁻¹' ↑(Finsupp.support 0)) := ⋯) : Finsupp.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 ⁻¹' ↑(Finsupp.single (f a) m).support)) : Finsupp.comapDomain f (Finsupp.single (f a) m) hif = Finsupp.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)) : 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} [AddZeroClass M] {f : α → β} (hf : Function.Injective f) (v₁ v₂ : β →₀ M) : Finsupp.comapDomain f (v₁ + v₂) ⋯ = Finsupp.comapDomain f v₁ ⋯ + Finsupp.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) : (Finsupp.comapDomain.addMonoidHom hf) x = Finsupp.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) : Finsupp.mapDomain f (Finsupp.comapDomain f l ⋯) = l

Declarations about finitely supported functions whose support is an Option type

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

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

Equations

• f.some = Finsupp.comapDomain some f ⋯

@[simp]

theorem Finsupp.some_apply {α : Type u_1} {M : Type u_5} [Zero M] (f : Option α →₀ M) (a : α) : f.some a = f (some a)

@[simp]

theorem Finsupp.some_zero {α : Type u_1} {M : Type u_5} [Zero M] : Finsupp.some 0 = 0

@[simp]

theorem Finsupp.some_add {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f g : Option α →₀ 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 = Finsupp.single a m

theorem Finsupp.prod_option_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [CommMonoid N] (f : Option α →₀ M) (b : Option α → M → N) (h_zero : ∀ (o : Option α), b o 0 = 1) (h_add : ∀ (o : Option α) (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 {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] (f : Option α →₀ M) (b : Option α → M → N) (h_zero : ∀ (o : Option α), b o 0 = 0) (h_add : ∀ (o : Option α) (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.sum_option_index_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} [Semiring R] [AddCommMonoid M] [Module R M] (f : Option α →₀ R) (b : Option α → M) : (f.sum fun (o : Option α) (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) [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 : α) : (Finsupp.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) : ⇑(Finsupp.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) : Finsupp.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) : Finsupp.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) : (Finsupp.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) : (Finsupp.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) : (Finsupp.filter p f).support = Finset.filter (fun (x : α) => p x) f.support

theorem Finsupp.filter_zero {α : Type u_1} {M : Type u_5} [Zero M] (p : α → Prop) [DecidablePred p] : Finsupp.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) : Finsupp.filter p (Finsupp.single a b) = Finsupp.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) : Finsupp.filter p (Finsupp.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) : (Finsupp.filter p f).prod g = ∏ x ∈ (Finsupp.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) : (Finsupp.filter p f).sum g = ∑ x ∈ (Finsupp.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) : (Finsupp.filter p f).prod g * (Finsupp.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) : (Finsupp.filter p f).sum g + (Finsupp.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 / (Finsupp.filter p f).prod g = (Finsupp.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 - (Finsupp.filter p f).sum g = (Finsupp.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] : Finsupp.filter p f + 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) : 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_not_mem_frange {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} : 0 ∉ f.frange

theorem Finsupp.frange_single {α : Type u_1} {M : Type u_5} [Zero M] {x : α} {y : M} : (Finsupp.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} : (Finsupp.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} : (Finsupp.subtypeDomain p v) a = v ↑a

@[simp]

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

theorem Finsupp.subtypeDomain_eq_zero_iff' {α : Type u_1} {M : Type u_5} [Zero M] {p : α → Prop} {f : α →₀ M} : Finsupp.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) : Finsupp.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) : ((Finsupp.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) : ((Finsupp.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} : Finsupp.subtypeDomain p (v + v') = Finsupp.subtypeDomain p v + Finsupp.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} : Finsupp.filter p (v + v') = Finsupp.filter p v + Finsupp.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} : Finsupp.subtypeDomain p (∑ c ∈ s, h c) = ∑ c ∈ s, Finsupp.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} : 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} [AddCommMonoid M] {p : α → Prop} [DecidablePred p] (s : Finset ι) (f : ι → α →₀ M) : Finsupp.filter p (∑ a ∈ s, f a) = ∑ a ∈ s, Finsupp.filter p (f a)

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

@[simp]

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

@[simp]

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

@[simp]

theorem Finsupp.single_neg {α : Type u_1} {G : Type u_9} [AddGroup G] (a : α) (b : G) : Finsupp.single a (-b) = -Finsupp.single a b

@[simp]

theorem Finsupp.single_sub {α : Type u_1} {G : Type u_9} [AddGroup G] (a : α) (b₁ b₂ : G) : Finsupp.single a (b₁ - b₂) = Finsupp.single a b₁ - Finsupp.single a b₂

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Finsupp.filter_sub {α : Type u_1} {G : Type u_9} [AddGroup G] (p : α → Prop) [DecidablePred p] (f₁ f₂ : α →₀ G) : Finsupp.filter p (f₁ - f₂) = Finsupp.filter p f₁ - Finsupp.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.curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid 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

• f.curry = f.sum fun (p : α × β) (c : M) => Finsupp.single p.1 (Finsupp.single p.2 c)

@[simp]

theorem Finsupp.curry_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (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} [AddCommMonoid M] [AddCommMonoid N] (f : α × β →₀ M) (g : α → β → M → N) (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} [AddCommMonoid 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 = f.sum fun (a : α) (g : β →₀ M) => g.sum fun (b : β) (c : M) => Finsupp.single (a, b) c

def Finsupp.finsuppProdEquiv {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid 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 := ⋯ }

theorem Finsupp.filter_curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (f : α × β →₀ M) (p : α → Prop) [DecidablePred p] : (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} [AddCommMonoid M] [DecidableEq α] (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

• f.sumElim g = Finsupp.onFinset (Finset.map { toFun := Sum.inl, inj' := ⋯ } f.support ∪ Finset.map { toFun := Sum.inr, inj' := ⋯ } g.support) (Sum.elim ⇑f ⇑g) ⋯

@[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

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 : (α →₀ γ) × (β →₀ γ)) : 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 ⋯)

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

theorem Finsupp.snd_sumFinsuppEquivProdFinsupp {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α ⊕ β →₀ γ) (y : β) : (Finsupp.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 : α) : (Finsupp.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 : β) : (Finsupp.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)) : Finsupp.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) : Finsupp.sumFinsuppAddEquivProdFinsupp f = (Finsupp.comapDomain Sum.inl f ⋯, Finsupp.comapDomain Sum.inr f ⋯)

theorem Finsupp.fst_sumFinsuppAddEquivProdFinsupp {M : Type u_5} [AddMonoid M] {α : Type u_13} {β : Type u_14} (f : α ⊕ β →₀ M) (x : α) : (Finsupp.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 : β) : (Finsupp.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 : α) : (Finsupp.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 : β) : (Finsupp.sumFinsuppAddEquivProdFinsupp.symm fg) (Sum.inr y) = 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] [MonoidWithZero R] [MulActionWithZero R M] (a b : α) (f : α → M) (r : R) : (Finsupp.single a 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} [Monoid G] [MulAction G α] [AddCommMonoid M] : 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

• Finsupp.comapSMul = { smul := fun (g : G) => Finsupp.mapDomain fun (x : α) => g • x }

theorem Finsupp.comapSMul_def {α : Type u_1} {M : Type u_5} {G : Type u_9} [Monoid G] [MulAction G α] [AddCommMonoid M] (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} [Monoid G] [MulAction G α] [AddCommMonoid M] (g : G) (a : α) (b : M) : g • Finsupp.single a b = Finsupp.single (g • a) b

def Finsupp.comapMulAction {α : Type u_1} {M : Type u_5} {G : Type u_9} [Monoid G] [MulAction G α] [AddCommMonoid M] : MulAction G (α →₀ M)

Finsupp.comapSMul is multiplicative

Equations

• Finsupp.comapMulAction = MulAction.mk ⋯ ⋯

def Finsupp.comapDistribMulAction {α : Type u_1} {M : Type u_5} {G : Type u_9} [Monoid G] [MulAction G α] [AddCommMonoid M] : DistribMulAction G (α →₀ M)

Finsupp.comapSMul is distributive

Equations

• Finsupp.comapDistribMulAction = DistribMulAction.mk ⋯ ⋯

@[simp]

theorem Finsupp.comapSMul_apply {α : Type u_1} {M : Type u_5} {G : Type u_9} [Group G] [MulAction G α] [AddCommMonoid M] (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] [SMulZeroClass R M] : SMulZeroClass R (α →₀ M)

Equations

• Finsupp.smulZeroClass = SMulZeroClass.mk ⋯

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] [SMulZeroClass R 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] [SMulZeroClass R 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] [SMulZeroClass R M] {k : R} (hk : IsSMulRegular M k) : IsSMulRegular (α →₀ M) k

instance Finsupp.faithfulSMul {α : Type u_1} {M : Type u_5} {R : Type u_11} [Nonempty α] [Zero M] [SMulZeroClass R M] [FaithfulSMul R M] : FaithfulSMul R (α →₀ M)

Equations

• ⋯ = ⋯

instance Finsupp.instSMulWithZero {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero R] [Zero M] [SMulWithZero R M] : SMulWithZero R (α →₀ M)

Equations

• Finsupp.instSMulWithZero = SMulWithZero.mk ⋯

instance Finsupp.distribSMul (α : Type u_1) (M : Type u_5) {R : Type u_11} [AddZeroClass M] [DistribSMul R M] : DistribSMul R (α →₀ M)

Equations

• Finsupp.distribSMul α M = DistribSMul.mk ⋯

instance Finsupp.distribMulAction (α : Type u_1) (M : Type u_5) {R : Type u_11} [Monoid R] [AddMonoid M] [DistribMulAction R M] : DistribMulAction R (α →₀ M)

Equations

• Finsupp.distribMulAction α M = DistribMulAction.mk ⋯ ⋯

instance Finsupp.isScalarTower (α : Type u_1) (M : Type u_5) {R : Type u_11} {S : Type u_12} [Zero M] [SMulZeroClass R M] [SMulZeroClass S M] [SMul R S] [IsScalarTower R S M] : IsScalarTower R S (α →₀ M)

Equations

• ⋯ = ⋯

instance Finsupp.smulCommClass (α : Type u_1) (M : Type u_5) {R : Type u_11} {S : Type u_12} [Zero M] [SMulZeroClass R M] [SMulZeroClass S M] [SMulCommClass R S M] : SMulCommClass R S (α →₀ M)

Equations

• ⋯ = ⋯

instance Finsupp.isCentralScalar (α : Type u_1) (M : Type u_5) {R : Type u_11} [Zero M] [SMulZeroClass R M] [SMulZeroClass Rᵐᵒᵖ M] [IsCentralScalar R M] : IsCentralScalar R (α →₀ M)

Equations

• ⋯ = ⋯

instance Finsupp.module (α : Type u_1) (M : Type u_5) {R : Type u_11} [Semiring R] [AddCommMonoid M] [Module R M] : Module R (α →₀ M)

Equations

• Finsupp.module α M = Module.mk ⋯ ⋯

theorem Finsupp.support_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} [AddMonoid M] [SMulZeroClass R M] {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} [Semiring R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors 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} [DecidablePred p] {x✝ : Monoid R} [AddMonoid M] [DistribMulAction R M] {b : R} {v : α →₀ M} : Finsupp.filter p (b • v) = b • Finsupp.filter p v

theorem Finsupp.mapDomain_smul {α : Type u_1} {β : Type u_2} {M : Type u_5} {R : Type u_11} {x✝ : Monoid R} [AddCommMonoid M] [DistribMulAction R M] {f : α → β} (b : R) (v : α →₀ M) : Finsupp.mapDomain f (b • v) = b • Finsupp.mapDomain f v

@[simp]

theorem Finsupp.smul_single {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] [SMulZeroClass R M] (c : R) (a : α) (b : M) : c • Finsupp.single a b = Finsupp.single a (c • b)

theorem Finsupp.smul_single' {α : Type u_1} {R : Type u_11} {x✝ : Semiring R} (c : R) (a : α) (b : R) : c • Finsupp.single a b = 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✝ : Monoid R} [AddMonoid M] [DistribMulAction R M] [AddMonoid N] [DistribMulAction R N] {f : M → N} {hf : f 0 = 0} (c : R) (v : α →₀ M) (hsmul : ∀ (x : M), f (c • x) = c • f x) : Finsupp.mapRange f hf (c • v) = c • Finsupp.mapRange f hf v

theorem Finsupp.smul_single_one {α : Type u_1} {R : Type u_11} [Semiring R] (a : α) (b : R) : b • Finsupp.single a 1 = Finsupp.single a b

theorem Finsupp.comapDomain_smul {α : Type u_1} {β : Type u_2} {M : Type u_5} {R : Type u_11} [AddMonoid M] [Monoid R] [DistribMulAction R M] {f : α → β} (r : R) (v : β →₀ M) (hfv : Set.InjOn f (f ⁻¹' ↑v.support)) (hfrv : Set.InjOn f (f ⁻¹' ↑(r • v).support) := ⋯) : Finsupp.comapDomain f (r • v) hfrv = r • Finsupp.comapDomain f v hfv

theorem Finsupp.comapDomain_smul_of_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} {R : Type u_11} [AddMonoid M] [Monoid R] [DistribMulAction R M] {f : α → β} (hf : Function.Injective f) (r : R) (v : β →₀ M) : Finsupp.comapDomain f (r • v) ⋯ = r • Finsupp.comapDomain f v ⋯

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} [Semiring R] [AddCommMonoid M] {g : α →₀ R} {b : R} {h : α → R → M} (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} [AddMonoid M] [DistribSMul R M] [AddCommMonoid N] {g : α →₀ M} {b : R} {h : α → M → N} (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} [AddMonoid M] [AddCommMonoid N] [DistribSMul R M] {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} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_13} [NoZeroSMulDivisors R M] : NoZeroSMulDivisors R (ι →₀ M)

Equations

• ⋯ = ⋯

def Finsupp.DistribMulActionHom.single {α : Type u_1} {M : Type u_5} {R : Type u_11} [Monoid R] [AddMonoid M] [DistribMulAction R M] (a : α) : M →+[R] α →₀ M

Finsupp.single as a DistribMulActionSemiHom.

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

Equations

• Finsupp.DistribMulActionHom.single a = { toFun := (↑(Finsupp.singleAddHom a)).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem Finsupp.distribMulActionHom_ext {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} [Monoid R] [AddMonoid M] [AddMonoid N] [DistribMulAction R M] [DistribMulAction R N] {f g : (α →₀ M) →+[R] N} (h : ∀ (a : α) (m : M), f (Finsupp.single a m) = g (Finsupp.single a m)) : f = g

theorem Finsupp.distribMulActionHom_ext' {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} [Monoid R] [AddMonoid M] [AddMonoid N] [DistribMulAction R M] [DistribMulAction R N] {f g : (α →₀ M) →+[R] N} (h : ∀ (a : α), f.comp (Finsupp.DistribMulActionHom.single a) = g.comp (Finsupp.DistribMulActionHom.single a)) : f = g

See note [partially-applied ext lemmas].

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_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.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.subtypeDomain_piecewise {α : Type u_1} {M : Type u_13} [Zero M] {P : α → Prop} [DecidablePred P] (f : Subtype P →₀ 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} [DecidablePred P] (f : Subtype P →₀ M) (g : { a : α // ¬P a } →₀ M) : Finsupp.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_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

@[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

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 = Finsupp.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) : Finsupp.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) : (Finsupp.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) : (Finsupp.single a m).extendDomain = Finsupp.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.

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 = Finsupp.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) : (Finsupp.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) : (Finsupp.sigmaFinsuppAddEquivPiFinsupp f j) i = f ⟨j, i⟩