Documentation

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

Instances For

theorem Finsupp.mk_mem_graph_iff {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {m : M} {f : α →₀ M} :

(a, m) ∈ f.graph ↔ f a = m ∧ m ≠ 0

@[simp]

theorem Finsupp.mem_graph_iff {α : Type u_1} {M : Type u_5} [Zero M] {c : α × M} {f : α →₀ M} :

c ∈ f.graph ↔ f c.1 = c.2 ∧ c.2 ≠ 0

theorem Finsupp.mk_mem_graph {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) {a : α} (ha : a ∈ f.support) :

(a, f a) ∈ f.graph

theorem Finsupp.apply_eq_of_mem_graph {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {m : M} {f : α →₀ M} (h : (a, m) ∈ f.graph) :

f a = m

@[simp]

theorem Finsupp.notMem_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_12) (M : Type u_13) [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` #

theorem Finsupp.mapRange_multiset_sum {α : Type u_1} {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] {F : Type u_12} [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_6} [AddCommMonoid M] [AddCommMonoid N] {F : Type u_12} [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)

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

Instances For

@[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 fun₀ | a => b) = fun₀ | 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_6} [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_6} [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

Instances For

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

Instances For

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 fun₀ | a => b) = fun₀ | 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

Instances For

@[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_6} [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_6} [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_6} [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_6} [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_6} [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_6} [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_12} {β : Type u_13} (f : α ↪ β) :

(α →₀ ℕ) ↪ β →₀ ℕ

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

Equations

Instances For

@[simp]

theorem Finsupp.mapDomainEmbedding_apply {α : Type u_12} {β : Type u_13} (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_6} [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_6} [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_12} [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

Instances For

@[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_6} [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 ⁻¹' ↑(fun₀ | f a => m).support)) :

comapDomain f (fun₀ | f a => m) hif = fun₀ | a => m

theorem Finsupp.comapDomain_surjective {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] [Finite β] {f : α → β} (hf : Function.Injective f) :

Function.Surjective fun (l : β →₀ M) => comapDomain f l ⋯

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

Instances For

@[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.mapDomain_comapDomain_nat_add_one {M : Type u_5} [AddCommMonoid M] (l : ℕ →₀ M) :

mapDomain (fun (x : ℕ) => x + 1) ((comapDomain.addMonoidHom ⋯) l) = erase 0 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

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

x ∈ Set.range (mapDomain f) ↔ ∀ b ∉ Set.range f, x b = 0

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

Instances For

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 fun₀ | a => b) = fun₀ | 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 fun₀ | a => b) = 0

theorem Finsupp.prod_filter_index {α : Type u_1} {M : Type u_5} {N : Type u_6} [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_6} [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_6} [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_6} [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_8} [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_8} [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

Instances For

@[simp]

theorem Finsupp.mem_frange {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {y : M} :

y ∈ f.frange ↔ y ≠ 0 ∧ y ∈ Set.range ⇑f

theorem Finsupp.zero_notMem_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} :

(fun₀ | x => y).frange ⊆ {y}

theorem Finsupp.mem_frange_of_mem {α : Type u_1} {M : Type u_5} [Zero M] {x : α} {f : α →₀ M} (h : x ∈ f.support) :

f x ∈ f.frange

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

Set.range ⇑f ⊆ insert 0 ↑f.frange

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

(Set.range ⇑f).Finite

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

Instances For

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

Instances For

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

(α →₀ M) →+ α →₀ M

Finsupp.filter as an AddMonoidHom.

Equations

Instances For

@[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_6} [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, fun₀ | i => f i

@[simp]

theorem Finsupp.subtypeDomain_neg {α : Type u_1} {G : Type u_8} [AddGroup G] {p : α → Prop} {v : α →₀ G} :

subtypeDomain p (-v) = -subtypeDomain p v

@[simp]

theorem Finsupp.subtypeDomain_sub {α : Type u_1} {G : Type u_8} [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_8} [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_8} [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

Instances For

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

(fun₀ | a => fun₀ | b => m).uncurry = fun₀ | (a, b) => m

theorem Finsupp.sum_uncurry_index {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [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_6} [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} [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

Instances For

@[simp]

theorem Finsupp.curry_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [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} [Zero M] [DecidableEq α] (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} [Zero M] (f : α →₀ β →₀ M) :

f.uncurry.curry = f

@[simp]

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

f.curry.uncurry = f

@[simp]

theorem Finsupp.curry_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (a : α × β) (m : M) :

(fun₀ | a => m).curry = fun₀ | a.1 => fun₀ | a.2 => m

theorem Finsupp.sum_curry_index {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [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.curryEquiv {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] :

(α × β →₀ M) ≃ (α →₀ β →₀ M)

The equivalence between α × β →₀ M and α →₀ β →₀ M given by currying/uncurrying.

Equations

Instances For

@[simp]

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

curryEquiv f = f.curry

@[simp]

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

curryEquiv.symm f = f.uncurry

@[deprecated Finsupp.curryEquiv (since := "2026-01-03")]

def Finsupp.finsuppProdEquiv {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] :

(α × β →₀ M) ≃ (α →₀ β →₀ M)

Alias of Finsupp.curryEquiv.

The equivalence between α × β →₀ M and α →₀ β →₀ M given by currying/uncurrying.

Equations

Instances For

theorem Finsupp.filter_curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α × β →₀ M) (p : α → Prop) [DecidablePred p] :

(filter (fun (a : α × β) => p a.1) f).curry = filter p f.curry

noncomputable def Finsupp.curryAddEquiv {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] :

(α × β →₀ M) ≃+ (α →₀ β →₀ M)

The additive monoid isomorphism between α × β →₀ M and α →₀ β →₀ M given by currying/uncurrying.

Equations

Instances For

@[simp]

theorem Finsupp.curryAddEquiv_symm_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] (f : α →₀ β →₀ M) :

curryAddEquiv.symm f = f.uncurry

@[simp]

theorem Finsupp.coe_curryAddEquiv {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] :

⇑curryAddEquiv = Finsupp.curry

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

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

α ⊕ β →₀ γ

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

Equations

Instances For

@[simp]

theorem Finsupp.sumElim_support {α : Type u_12} {β : Type u_13} {γ : Type u_14} [Zero γ] (f : α →₀ γ) (g : β →₀ γ) :

(f.sumElim g).support = f.support.disjSum g.support

@[simp]

theorem Finsupp.coe_sumElim {α : Type u_12} {β : Type u_13} {γ : Type u_14} [Zero γ] (f : α →₀ γ) (g : β →₀ γ) :

⇑(f.sumElim g) = Sum.elim ⇑f ⇑g

theorem Finsupp.sumElim_apply {α : Type u_12} {β : Type u_13} {γ : Type u_14} [Zero γ] (f : α →₀ γ) (g : β →₀ γ) (x : α ⊕ β) :

(f.sumElim g) x = Sum.elim (⇑f) (⇑g) x

theorem Finsupp.sumElim_inl {α : Type u_12} {β : Type u_13} {γ : Type u_14} [Zero γ] (f : α →₀ γ) (g : β →₀ γ) (x : α) :

(f.sumElim g) (Sum.inl x) = f x

theorem Finsupp.sumElim_inr {α : Type u_12} {β : Type u_13} {γ : Type u_14} [Zero γ] (f : α →₀ γ) (g : β →₀ γ) (x : β) :

(f.sumElim g) (Sum.inr x) = g x

theorem Finsupp.prod_sumElim {ι₁ : Type u_12} {ι₂ : Type u_13} {α : Type u_14} {M : Type u_15} [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_12} {ι₂ : Type u_13} {α : Type u_14} {M : Type u_15} [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_12} {β : Type u_13} {γ : Type u_14} [Zero γ] :

(α ⊕ β →₀ γ) ≃ (α →₀ γ) × (β →₀ γ)

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

This is the Finsupp version of Equiv.sum_arrow_equiv_prod_arrow.

Equations

Instances For

@[simp]

theorem Finsupp.sumFinsuppEquivProdFinsupp_symm_apply {α : Type u_12} {β : Type u_13} {γ : Type u_14} [Zero γ] (fg : (α →₀ γ) × (β →₀ γ)) :

sumFinsuppEquivProdFinsupp.symm fg = fg.1.sumElim fg.2

@[simp]

theorem Finsupp.sumFinsuppEquivProdFinsupp_apply {α : Type u_12} {β : Type u_13} {γ : Type u_14} [Zero γ] (f : α ⊕ β →₀ γ) :

sumFinsuppEquivProdFinsupp f = (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)

theorem Finsupp.fst_sumFinsuppEquivProdFinsupp {α : Type u_12} {β : Type u_13} {γ : Type u_14} [Zero γ] (f : α ⊕ β →₀ γ) (x : α) :

(sumFinsuppEquivProdFinsupp f).1 x = f (Sum.inl x)

theorem Finsupp.snd_sumFinsuppEquivProdFinsupp {α : Type u_12} {β : Type u_13} {γ : Type u_14} [Zero γ] (f : α ⊕ β →₀ γ) (y : β) :

(sumFinsuppEquivProdFinsupp f).2 y = f (Sum.inr y)

theorem Finsupp.sumFinsuppEquivProdFinsupp_symm_inl {α : Type u_12} {β : Type u_13} {γ : Type u_14} [Zero γ] (fg : (α →₀ γ) × (β →₀ γ)) (x : α) :

(sumFinsuppEquivProdFinsupp.symm fg) (Sum.inl x) = fg.1 x

theorem Finsupp.sumFinsuppEquivProdFinsupp_symm_inr {α : Type u_12} {β : Type u_13} {γ : Type u_14} [Zero γ] (fg : (α →₀ γ) × (β →₀ γ)) (y : β) :

(sumFinsuppEquivProdFinsupp.symm fg) (Sum.inr y) = fg.2 y

def Finsupp.sumFinsuppAddEquivProdFinsupp {M : Type u_5} [AddMonoid M] {α : Type u_12} {β : Type u_13} :

(α ⊕ β →₀ M) ≃+ (α →₀ M) × (β →₀ M)

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

This is the Finsupp version of Equiv.sum_arrow_equiv_prod_arrow.

Equations

Instances For

@[simp]

theorem Finsupp.sumFinsuppAddEquivProdFinsupp_symm_apply {M : Type u_5} [AddMonoid M] {α : Type u_12} {β : Type u_13} (fg : (α →₀ M) × (β →₀ M)) :

sumFinsuppAddEquivProdFinsupp.symm fg = fg.1.sumElim fg.2

@[simp]

theorem Finsupp.sumFinsuppAddEquivProdFinsupp_apply {M : Type u_5} [AddMonoid M] {α : Type u_12} {β : Type u_13} (f : α ⊕ β →₀ M) :

sumFinsuppAddEquivProdFinsupp f = (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)

theorem Finsupp.fst_sumFinsuppAddEquivProdFinsupp {M : Type u_5} [AddMonoid M] {α : Type u_12} {β : Type u_13} (f : α ⊕ β →₀ M) (x : α) :

(sumFinsuppAddEquivProdFinsupp f).1 x = f (Sum.inl x)

theorem Finsupp.snd_sumFinsuppAddEquivProdFinsupp {M : Type u_5} [AddMonoid M] {α : Type u_12} {β : Type u_13} (f : α ⊕ β →₀ M) (y : β) :

(sumFinsuppAddEquivProdFinsupp f).2 y = f (Sum.inr y)

theorem Finsupp.sumFinsuppAddEquivProdFinsupp_symm_inl {M : Type u_5} [AddMonoid M] {α : Type u_12} {β : Type u_13} (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_12} {β : Type u_13} (fg : (α →₀ M) × (β →₀ M)) (y : β) :

(sumFinsuppAddEquivProdFinsupp.symm fg) (Sum.inr y) = fg.2 y

instance Finsupp.uniqueOfRight {α : Type u_1} {R : Type u_10} [Zero R] [Subsingleton R] :

Unique (α →₀ R)

The Finsupp version of Pi.unique.

Equations

instance Finsupp.uniqueOfLeft {α : Type u_1} {R : Type u_10} [Zero R] [IsEmpty α] :

Unique (α →₀ R)

The Finsupp version of Pi.uniqueOfIsEmpty.

Equations

def Finsupp.piecewise {α : Type u_1} {M : Type u_12} [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

Instances For

@[simp]

theorem Finsupp.piecewise_apply {α : Type u_1} {M : Type u_12} [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_12} [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_12} [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_12} [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_12} [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

Instances For

@[simp]

theorem Finsupp.extendDomain_apply {α : Type u_1} {M : Type u_12} [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_12} [Zero M] {P : α → Prop} [DecidablePred P] (f : Subtype P →₀ M) :

f.extendDomain.support = Finset.map (Function.Embedding.subtype P) f.support

@[deprecated Finsupp.extendDomain_apply (since := "2025-12-15")]

theorem Finsupp.extendDomain_toFun {α : Type u_1} {M : Type u_12} [Zero M] {P : α → Prop} [DecidablePred P] (f : Subtype P →₀ M) (a : α) :

f.extendDomain a = if h : P a then f ⟨a, h⟩ else 0

Alias of Finsupp.extendDomain_apply.

theorem Finsupp.extendDomain_eq_embDomain_subtype {α : Type u_1} {M : Type u_12} [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_12} [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_12} [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_12} [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_12} [Zero M] {P : α → Prop} [DecidablePred P] (a : Subtype P) (m : M) :

(fun₀ | a => m).extendDomain = fun₀ | ↑a => m

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

Instances For

@[simp]

theorem Finsupp.restrictSupportEquiv_apply {α : Type u_1} (s : Set α) (M : Type u_12) [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_12) [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_12) [AddCommMonoid M] (a : ↑s) (x : M) :

↑((restrictSupportEquiv s M).symm fun₀ | a => x) = fun₀ | ↑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

Instances For

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

Instances For

theorem Finsupp.split_apply {ι : Type u_4} {M : Type u_5} {αs : ι → Type u_12} [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_12} [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

Instances For

theorem Finsupp.mem_splitSupport_iff_nonzero {ι : Type u_4} {M : Type u_5} {αs : ι → Type u_12} [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_6} {αs : ι → Type u_12} [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

Instances For

theorem Finsupp.sigma_support {ι : Type u_4} {M : Type u_5} {αs : ι → Type u_12} [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_6} {αs : ι → Type u_12} [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_13} [Fintype η] {ιs : η → Type u_14} [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

Instances For

@[simp]

theorem Finsupp.sigmaFinsuppEquivPiFinsupp_apply {α : Type u_1} {η : Type u_13} [Fintype η] {ιs : η → Type u_14} [Zero α] (f : (j : η) × ιs j →₀ α) (j : η) (i : ιs j) :

(sigmaFinsuppEquivPiFinsupp f j) i = f ⟨j, i⟩

noncomputable def Finsupp.sigmaFinsuppAddEquivPiFinsupp {η : Type u_13} [Fintype η] {α : Type u_15} {ιs : η → Type u_16} [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

Instances For