mathlib3 documentation

data.finsupp.basic

Miscellaneous definitions, lemmas, and constructions using finsupp #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main declarations #

Implementation notes #

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

TODO #

Declarations about graph #

def finsupp.graph {α : Type u_1} {M : Type u_5} [has_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
theorem finsupp.mk_mem_graph_iff {α : Type u_1} {M : Type u_5} [has_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} [has_zero M] {c : α × M} {f : α →₀ M} :
c f.graph f c.fst = c.snd c.snd 0
theorem finsupp.mk_mem_graph {α : Type u_1} {M : Type u_5} [has_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} [has_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} [has_zero M] (a : α) (f : α →₀ M) :
(a, 0) f.graph
@[simp]
theorem finsupp.image_fst_graph {α : Type u_1} {M : Type u_5} [has_zero M] [decidable_eq α] (f : α →₀ M) :
@[simp]
theorem finsupp.graph_inj {α : Type u_1} {M : Type u_5} [has_zero M] {f g : α →₀ M} :
f.graph = g.graph f = g
@[simp]
theorem finsupp.graph_zero {α : Type u_1} {M : Type u_5} [has_zero M] :
@[simp]
theorem finsupp.graph_eq_empty {α : Type u_1} {M : Type u_5} [has_zero M] {f : α →₀ M} :
f.graph = f = 0

Declarations about map_range #

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

finsupp.map_range as an equiv.

Equations
theorem finsupp.map_range.equiv_trans {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [has_zero M] [has_zero N] [has_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) :
@[simp]
theorem finsupp.map_range.equiv_symm {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [has_zero N] (f : M N) (hf : f 0 = 0) (hf' : (f.symm) 0 = 0) :
noncomputable def finsupp.map_range.zero_hom {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [has_zero N] (f : zero_hom M N) :
zero_hom →₀ M) →₀ N)

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

Equations
@[simp]
theorem finsupp.map_range.zero_hom_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] [has_zero N] (f : zero_hom M N) (g : α →₀ M) :
theorem finsupp.map_range.zero_hom_comp {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [has_zero M] [has_zero N] [has_zero P] (f : zero_hom N P) (f₂ : zero_hom M N) :
noncomputable def finsupp.map_range.add_monoid_hom {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (f : M →+ N) :
→₀ M) →+ α →₀ N

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

Equations
@[simp]
theorem finsupp.map_range_multiset_sum {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (f : M →+ N) (m : multiset →₀ M)) :
theorem finsupp.map_range_finset_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (f : M →+ N) (s : finset ι) (g : ι α →₀ M) :
finsupp.map_range f _ (s.sum (λ (x : ι), g x)) = s.sum (λ (x : ι), finsupp.map_range f _ (g x))
noncomputable def finsupp.map_range.add_equiv {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (f : M ≃+ N) :
→₀ M) ≃+ →₀ N)

finsupp.map_range.add_monoid_hom as an equiv.

Equations
@[simp]
theorem finsupp.map_range.add_equiv_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (f : M ≃+ N) (g : α →₀ M) :

Declarations about equiv_congr_left #

def finsupp.equiv_map_domain {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (l : α →₀ M) :
β →₀ M

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

Equations
@[simp]
theorem finsupp.equiv_map_domain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (l : α →₀ M) (b : β) :
theorem finsupp.equiv_map_domain_symm_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (l : β →₀ M) (a : α) :
@[simp]
theorem finsupp.equiv_map_domain_refl {α : Type u_1} {M : Type u_5} [has_zero M] (l : α →₀ M) :
theorem finsupp.equiv_map_domain_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [has_zero M] (f : α β) (g : β γ) (l : α →₀ M) :
theorem finsupp.equiv_map_domain_trans' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [has_zero M] (f : α β) (g : β γ) :
@[simp]
theorem finsupp.equiv_map_domain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (a : α) (b : M) :
@[simp]
theorem finsupp.equiv_map_domain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] {f : α β} :
def finsupp.equiv_congr_left {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_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.Pi_congr_left.

Equations
@[simp]
theorem finsupp.equiv_congr_left_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (l : α →₀ M) :
@[simp]
theorem finsupp.equiv_congr_left_symm {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) :
@[simp, norm_cast]
theorem nat.cast_finsupp_prod {α : Type u_1} {M : Type u_5} {R : Type u_11} [has_zero M] (f : α →₀ M) [comm_semiring R] (g : α M ) :
(f.prod g) = f.prod (λ (a : α) (b : M), (g a b))
@[simp, norm_cast]
theorem nat.cast_finsupp_sum {α : Type u_1} {M : Type u_5} {R : Type u_11} [has_zero M] (f : α →₀ M) [comm_semiring R] (g : α M ) :
(f.sum g) = f.sum (λ (a : α) (b : M), (g a b))
@[simp, norm_cast]
theorem int.cast_finsupp_prod {α : Type u_1} {M : Type u_5} {R : Type u_11} [has_zero M] (f : α →₀ M) [comm_ring R] (g : α M ) :
(f.prod g) = f.prod (λ (a : α) (b : M), (g a b))
@[simp, norm_cast]
theorem int.cast_finsupp_sum {α : Type u_1} {M : Type u_5} {R : Type u_11} [has_zero M] (f : α →₀ M) [comm_ring R] (g : α M ) :
(f.sum g) = f.sum (λ (a : α) (b : M), (g a b))
@[simp, norm_cast]
theorem rat.cast_finsupp_sum {α : Type u_1} {M : Type u_5} {R : Type u_11} [has_zero M] (f : α →₀ M) [division_ring R] [char_zero R] (g : α M ) :
(f.sum g) = f.sum (λ (a : α) (b : M), (g a b))
@[simp, norm_cast]
theorem rat.cast_finsupp_prod {α : Type u_1} {M : Type u_5} {R : Type u_11} [has_zero M] (f : α →₀ M) [field R] [char_zero R] (g : α M ) :
(f.prod g) = f.prod (λ (a : α) (b : M), (g a b))

Declarations about map_domain #

noncomputable def finsupp.map_domain {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (f : α β) (v : α →₀ M) :
β →₀ M

Given f : α → β and v : α →₀ M, map_domain 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
theorem finsupp.map_domain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] {f : α β} (hf : function.injective f) (x : α →₀ M) (a : α) :
(finsupp.map_domain f x) (f a) = x a
theorem finsupp.map_domain_notin_range {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] {f : α β} (x : α →₀ M) (a : β) (h : a set.range f) :
@[simp]
theorem finsupp.map_domain_id {α : Type u_1} {M : Type u_5} [add_comm_monoid M] {v : α →₀ M} :
theorem finsupp.map_domain_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [add_comm_monoid M] {v : α →₀ M} {f : α β} {g : β γ} :
@[simp]
theorem finsupp.map_domain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] {f : α β} {a : α} {b : M} :
@[simp]
theorem finsupp.map_domain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] {f : α β} :
theorem finsupp.map_domain_congr {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] {v : α →₀ M} {f g : α β} (h : (x : α), x v.support f x = g x) :
theorem finsupp.map_domain_add {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] {v₁ v₂ : α →₀ M} {f : α β} :
@[simp]
theorem finsupp.map_domain_equiv_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] {f : α β} (x : α →₀ M) (a : β) :
@[simp]
theorem finsupp.map_domain.add_monoid_hom_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (f : α β) (v : α →₀ M) :
noncomputable def finsupp.map_domain.add_monoid_hom {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (f : α β) :
→₀ M) →+ β →₀ M

finsupp.map_domain is an add_monoid_hom.

Equations
theorem finsupp.map_domain_finset_sum {α : Type u_1} {β : Type u_2} {ι : Type u_4} {M : Type u_5} [add_comm_monoid M] {f : α β} {s : finset ι} {v : ι α →₀ M} :
finsupp.map_domain f (s.sum (λ (i : ι), v i)) = s.sum (λ (i : ι), finsupp.map_domain f (v i))
theorem finsupp.map_domain_sum {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [has_zero N] {f : α β} {s : α →₀ N} {v : α N α →₀ M} :
finsupp.map_domain f (s.sum v) = s.sum (λ (a : α) (b : N), finsupp.map_domain f (v a b))
theorem finsupp.map_domain_support {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] [decidable_eq β] {f : α β} {s : α →₀ M} :
theorem finsupp.map_domain_apply' {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (S : set α) {f : α β} (x : α →₀ M) (hS : (x.support) S) (hf : set.inj_on f S) {a : α} (ha : a S) :
(finsupp.map_domain f x) (f a) = x a
theorem finsupp.map_domain_support_of_inj_on {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] [decidable_eq β] {f : α β} (s : α →₀ M) (hf : set.inj_on f (s.support)) :
theorem finsupp.map_domain_support_of_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] [decidable_eq β] {f : α β} (hf : function.injective f) (s : α →₀ M) :
theorem finsupp.sum_map_domain_index {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid 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.map_domain f s).sum h = s.sum (λ (a : α) (m : M), h (f a) m)
theorem finsupp.prod_map_domain_index {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [comm_monoid 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.map_domain f s).prod h = s.prod (λ (a : α) (m : M), h (f a) m)
@[simp]
theorem finsupp.sum_map_domain_index_add_monoid_hom {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] {f : α β} {s : α →₀ M} (h : β M →+ N) :
(finsupp.map_domain f s).sum (λ (b : β) (m : M), (h b) m) = s.sum (λ (a : α) (m : M), (h (f a)) m)

A version of sum_map_domain_index that takes a bundled add_monoid_hom, rather than separate linearity hypotheses.

theorem finsupp.emb_domain_eq_map_domain {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (f : α β) (v : α →₀ M) :
theorem finsupp.prod_map_domain_index_inj {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [comm_monoid N] {f : α β} {s : α →₀ M} {h : β M N} (hf : function.injective f) :
(finsupp.map_domain f s).prod h = s.prod (λ (a : α) (b : M), h (f a) b)
theorem finsupp.sum_map_domain_index_inj {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] {f : α β} {s : α →₀ M} {h : β M N} (hf : function.injective f) :
(finsupp.map_domain f s).sum h = s.sum (λ (a : α) (b : M), h (f a) b)
theorem finsupp.map_domain_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] {f : α β} (hf : function.injective f) :
noncomputable def finsupp.map_domain_embedding {α : Type u_1} {β : Type u_2} (f : α β) :

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

Equations
@[simp]
theorem finsupp.map_domain_embedding_apply {α : Type u_1} {β : Type u_2} (f : α β) (v : α →₀ ) :
theorem finsupp.map_domain_map_range {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid N] (f : α β) (v : α →₀ M) (g : M N) (h0 : g 0 = 0) (hadd : (x y : M), g (x + y) = g x + g y) :

When g preserves addition, map_range and map_domain commute.

theorem finsupp.sum_update_add {α : Type u_1} {β : Type u_2} {ι : Type u_4} [add_comm_monoid α] [add_comm_monoid β] (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.map_domain_inj_on {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (S : set α) {f : α β} (hf : set.inj_on f S) :
theorem finsupp.equiv_map_domain_eq_map_domain {α : Type u_1} {β : Type u_2} {M : Type u_3} [add_comm_monoid M] (f : α β) (l : α →₀ M) :

Declarations about comap_domain #

@[simp]
theorem finsupp.comap_domain_support {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (l : β →₀ M) (hf : set.inj_on f (f ⁻¹' (l.support))) :
noncomputable def finsupp.comap_domain {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (l : β →₀ M) (hf : set.inj_on f (f ⁻¹' (l.support))) :
α →₀ M

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

Equations
@[simp]
theorem finsupp.comap_domain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (l : β →₀ M) (hf : set.inj_on f (f ⁻¹' (l.support))) (a : α) :
(finsupp.comap_domain f l hf) a = l (f a)
theorem finsupp.sum_comap_domain {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [has_zero M] [add_comm_monoid N] (f : α β) (l : β →₀ M) (g : β M N) (hf : set.bij_on f (f ⁻¹' (l.support)) (l.support)) :
(finsupp.comap_domain f l _).sum (g f) = l.sum g
theorem finsupp.eq_zero_of_comap_domain_eq_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (f : α β) (l : β →₀ M) (hf : set.bij_on f (f ⁻¹' (l.support)) (l.support)) :
@[simp]
theorem finsupp.comap_domain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (hif : set.inj_on f (f ⁻¹' (0.support)) := _) :

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

@[simp]
theorem finsupp.comap_domain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [has_zero M] (f : α β) (a : α) (m : M) (hif : set.inj_on f (f ⁻¹' ((finsupp.single (f a) m).support))) :
theorem finsupp.comap_domain_add {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_zero_class M] {f : α β} (v₁ v₂ : β →₀ M) (hv₁ : set.inj_on f (f ⁻¹' (v₁.support))) (hv₂ : set.inj_on f (f ⁻¹' (v₂.support))) (hv₁₂ : set.inj_on f (f ⁻¹' ((v₁ + v₂).support))) :
finsupp.comap_domain f (v₁ + v₂) hv₁₂ = finsupp.comap_domain f v₁ hv₁ + finsupp.comap_domain f v₂ hv₂
theorem finsupp.comap_domain_add_of_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_zero_class M] {f : α β} (hf : function.injective f) (v₁ v₂ : β →₀ M) :

A version of finsupp.comap_domain_add that's easier to use.

noncomputable def finsupp.comap_domain.add_monoid_hom {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_zero_class M] {f : α β} (hf : function.injective f) :
→₀ M) →+ α →₀ M

finsupp.comap_domain is an add_monoid_hom.

Equations
@[simp]
theorem finsupp.comap_domain.add_monoid_hom_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_zero_class M] {f : α β} (hf : function.injective f) (x : β →₀ M) :
theorem finsupp.map_domain_comap_domain {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (f : α β) (hf : function.injective f) (l : β →₀ M) (hl : (l.support) set.range f) :

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

noncomputable def finsupp.some {α : Type u_1} {M : Type u_5} [has_zero M] (f : option α →₀ M) :
α →₀ M

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

Equations
@[simp]
theorem finsupp.some_apply {α : Type u_1} {M : Type u_5} [has_zero M] (f : option α →₀ M) (a : α) :
@[simp]
theorem finsupp.some_zero {α : Type u_1} {M : Type u_5} [has_zero M] :
0.some = 0
@[simp]
theorem finsupp.some_add {α : Type u_1} {M : Type u_5} [add_comm_monoid 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} [has_zero M] (m : M) :
@[simp]
theorem finsupp.some_single_some {α : Type u_1} {M : Type u_5} [has_zero M] (a : α) (m : M) :
theorem finsupp.prod_option_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [comm_monoid 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 option.none (f option.none) * f.some.prod (λ (a : α), b (option.some a))
theorem finsupp.sum_option_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] [add_comm_monoid 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 option.none (f option.none) + f.some.sum (λ (a : α), b (option.some a))
theorem finsupp.sum_option_index_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} [semiring R] [add_comm_monoid M] [module R M] (f : option α →₀ R) (b : option α M) :
f.sum (λ (o : option α) (r : R), r b o) = f option.none b option.none + f.some.sum (λ (a : α) (r : R), r b (option.some a))

Declarations about filter #

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

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

Equations
theorem finsupp.filter_apply {α : Type u_1} {M : Type u_5} [has_zero M] (p : α Prop) (f : α →₀ M) (a : α) [D : decidable (p a)] :
(finsupp.filter p f) a = ite (p a) (f a) 0
theorem finsupp.filter_eq_indicator {α : Type u_1} {M : Type u_5} [has_zero M] (p : α Prop) (f : α →₀ M) :
(finsupp.filter p f) = {x : α | p x}.indicator f
theorem finsupp.filter_eq_zero_iff {α : Type u_1} {M : Type u_5} [has_zero M] (p : α Prop) (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} [has_zero M] (p : α Prop) (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} [has_zero M] (p : α Prop) (f : α →₀ M) {a : α} (h : p a) :
@[simp]
theorem finsupp.filter_apply_neg {α : Type u_1} {M : Type u_5} [has_zero M] (p : α Prop) (f : α →₀ M) {a : α} (h : ¬p a) :
@[simp]
theorem finsupp.support_filter {α : Type u_1} {M : Type u_5} [has_zero M] (p : α Prop) (f : α →₀ M) [D : decidable_pred p] :
theorem finsupp.filter_zero {α : Type u_1} {M : Type u_5} [has_zero M] (p : α Prop) :
@[simp]
theorem finsupp.filter_single_of_pos {α : Type u_1} {M : Type u_5} [has_zero M] (p : α Prop) {a : α} {b : M} (h : p a) :
@[simp]
theorem finsupp.filter_single_of_neg {α : Type u_1} {M : Type u_5} [has_zero M] (p : α Prop) {a : α} {b : M} (h : ¬p a) :
theorem finsupp.prod_filter_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] (p : α Prop) (f : α →₀ M) [comm_monoid N] (g : α M N) :
(finsupp.filter p f).prod g = (finsupp.filter p f).support.prod (λ (x : α), g x (f x))
theorem finsupp.sum_filter_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] (p : α Prop) (f : α →₀ M) [add_comm_monoid N] (g : α M N) :
(finsupp.filter p f).sum g = (finsupp.filter p f).support.sum (λ (x : α), g x (f x))
@[simp]
theorem finsupp.sum_filter_add_sum_filter_not {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] (p : α Prop) (f : α →₀ M) [add_comm_monoid N] (g : α M N) :
(finsupp.filter p f).sum g + (finsupp.filter (λ (a : α), ¬p a) f).sum g = f.sum g
@[simp]
theorem finsupp.prod_filter_mul_prod_filter_not {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] (p : α Prop) (f : α →₀ M) [comm_monoid N] (g : α M N) :
(finsupp.filter p f).prod g * (finsupp.filter (λ (a : α), ¬p a) f).prod g = f.prod g
@[simp]
theorem finsupp.sum_sub_sum_filter {α : Type u_1} {M : Type u_5} {G : Type u_9} [has_zero M] (p : α Prop) (f : α →₀ M) [add_comm_group G] (g : α M G) :
f.sum g - (finsupp.filter p f).sum g = (finsupp.filter (λ (a : α), ¬p a) f).sum g
@[simp]
theorem finsupp.prod_div_prod_filter {α : Type u_1} {M : Type u_5} {G : Type u_9} [has_zero M] (p : α Prop) (f : α →₀ M) [comm_group G] (g : α M G) :
f.prod g / (finsupp.filter p f).prod g = (finsupp.filter (λ (a : α), ¬p a) f).prod g
theorem finsupp.filter_pos_add_filter_neg {α : Type u_1} {M : Type u_5} [add_zero_class M] (f : α →₀ M) (p : α Prop) :
finsupp.filter p f + finsupp.filter (λ (a : α), ¬p a) f = f

Declarations about frange #

noncomputable def finsupp.frange {α : Type u_1} {M : Type u_5} [has_zero M] (f : α →₀ M) :

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

Equations
theorem finsupp.mem_frange {α : Type u_1} {M : Type u_5} [has_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} [has_zero M] {f : α →₀ M} :
theorem finsupp.frange_single {α : Type u_1} {M : Type u_5} [has_zero M] {x : α} {y : M} :

Declarations about subtype_domain #

noncomputable def finsupp.subtype_domain {α : Type u_1} {M : Type u_5} [has_zero M] (p : α Prop) (f : α →₀ M) :

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

Equations
@[simp]
theorem finsupp.support_subtype_domain {α : Type u_1} {M : Type u_5} [has_zero M] {p : α Prop} [D : decidable_pred p] {f : α →₀ M} :
@[simp]
theorem finsupp.subtype_domain_apply {α : Type u_1} {M : Type u_5} [has_zero M] {p : α Prop} {a : subtype p} {v : α →₀ M} :
@[simp]
theorem finsupp.subtype_domain_zero {α : Type u_1} {M : Type u_5} [has_zero M] {p : α Prop} :
theorem finsupp.subtype_domain_eq_zero_iff' {α : Type u_1} {M : Type u_5} [has_zero M] {p : α Prop} {f : α →₀ M} :
finsupp.subtype_domain p f = 0 (x : α), p x f x = 0
theorem finsupp.subtype_domain_eq_zero_iff {α : Type u_1} {M : Type u_5} [has_zero M] {p : α Prop} {f : α →₀ M} (hf : (x : α), x f.support p x) :
theorem finsupp.sum_subtype_domain_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] {p : α Prop} [add_comm_monoid N] {v : α →₀ M} {h : α M N} (hp : (x : α), x v.support p x) :
(finsupp.subtype_domain p v).sum (λ (a : subtype p) (b : M), h a b) = v.sum h
theorem finsupp.prod_subtype_domain_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [has_zero M] {p : α Prop} [comm_monoid N] {v : α →₀ M} {h : α M N} (hp : (x : α), x v.support p x) :
(finsupp.subtype_domain p v).prod (λ (a : subtype p) (b : M), h a b) = v.prod h
@[simp]
theorem finsupp.subtype_domain_add {α : Type u_1} {M : Type u_5} [add_zero_class M] {p : α Prop} {v v' : α →₀ M} :
noncomputable def finsupp.subtype_domain_add_monoid_hom {α : Type u_1} {M : Type u_5} [add_zero_class M] {p : α Prop} :

subtype_domain but as an add_monoid_hom.

Equations
noncomputable def finsupp.filter_add_hom {α : Type u_1} {M : Type u_5} [add_zero_class M] (p : α Prop) :
→₀ M) →+ α →₀ M

finsupp.filter as an add_monoid_hom.

Equations
@[simp]
theorem finsupp.filter_add {α : Type u_1} {M : Type u_5} [add_zero_class M] {p : α Prop} {v v' : α →₀ M} :
theorem finsupp.subtype_domain_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} [add_comm_monoid M] {p : α Prop} {s : finset ι} {h : ι α →₀ M} :
finsupp.subtype_domain p (s.sum (λ (c : ι), h c)) = s.sum (λ (c : ι), finsupp.subtype_domain p (h c))
theorem finsupp.subtype_domain_finsupp_sum {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [add_comm_monoid M] {p : α Prop} [has_zero N] {s : β →₀ N} {h : β N α →₀ M} :
finsupp.subtype_domain p (s.sum h) = s.sum (λ (c : β) (d : N), finsupp.subtype_domain p (h c d))
theorem finsupp.filter_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} [add_comm_monoid M] {p : α Prop} (s : finset ι) (f : ι α →₀ M) :
finsupp.filter p (s.sum (λ (a : ι), f a)) = s.sum (λ (a : ι), finsupp.filter p (f a))
theorem finsupp.filter_eq_sum {α : Type u_1} {M : Type u_5} [add_comm_monoid M] (p : α Prop) [D : decidable_pred p] (f : α →₀ M) :
finsupp.filter p f = (finset.filter p f.support).sum (λ (i : α), finsupp.single i (f i))
@[simp]
theorem finsupp.subtype_domain_neg {α : Type u_1} {G : Type u_9} [add_group G] {p : α Prop} {v : α →₀ G} :
@[simp]
theorem finsupp.subtype_domain_sub {α : Type u_1} {G : Type u_9} [add_group G] {p : α Prop} {v v' : α →₀ G} :
@[simp]
theorem finsupp.single_neg {α : Type u_1} {G : Type u_9} [add_group G] (a : α) (b : G) :
@[simp]
theorem finsupp.single_sub {α : Type u_1} {G : Type u_9} [add_group 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} [add_group G] (a : α) (f : α →₀ G) :
@[simp]
theorem finsupp.erase_sub {α : Type u_1} {G : Type u_9} [add_group 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} [add_group G] (p : α Prop) (f : α →₀ G) :
@[simp]
theorem finsupp.filter_sub {α : Type u_1} {G : Type u_9} [add_group G] (p : α Prop) (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} [add_comm_monoid M] {s : multiset →₀ M)} (a : α) :
a s.sum.support ( (f : α →₀ M) (H : f s), a f.support)
theorem finsupp.mem_support_finset_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} [add_comm_monoid M] {s : finset ι} {h : ι α →₀ M} (a : α) (ha : a (s.sum (λ (c : ι), h c)).support) :
(c : ι) (H : c s), a (h c).support

Declarations about curry and uncurry #

@[protected]
noncomputable def finsupp.curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid 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
@[simp]
theorem finsupp.curry_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid 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} [add_comm_monoid M] [add_comm_monoid 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 (λ (a : α) (f : β →₀ M), f.sum (g a)) = f.sum (λ (p : α × β) (c : M), g p.fst p.snd c)
@[protected]
noncomputable def finsupp.uncurry {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid 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
noncomputable def finsupp.finsupp_prod_equiv {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] :
× β →₀ M) →₀ β →₀ M)

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

Equations
theorem finsupp.filter_curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (f : α × β →₀ M) (p : α Prop) :
(finsupp.filter (λ (a : α × β), p a.fst) f).curry = finsupp.filter p f.curry
theorem finsupp.support_curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] [decidable_eq α] (f : α × β →₀ M) :

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

noncomputable def finsupp.sum_elim {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (f : α →₀ γ) (g : β →₀ γ) :
α β →₀ γ

finsupp.sum_elim f g maps inl x to f x and inr y to g y.

Equations
@[simp]
theorem finsupp.coe_sum_elim {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (f : α →₀ γ) (g : β →₀ γ) :
theorem finsupp.sum_elim_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (f : α →₀ γ) (g : β →₀ γ) (x : α β) :
theorem finsupp.sum_elim_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (f : α →₀ γ) (g : β →₀ γ) (x : α) :
(f.sum_elim g) (sum.inl x) = f x
theorem finsupp.sum_elim_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (f : α →₀ γ) (g : β →₀ γ) (x : β) :
(f.sum_elim g) (sum.inr x) = g x
@[simp]
theorem finsupp.sum_finsupp_equiv_prod_finsupp_symm_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (fg : →₀ γ) × →₀ γ)) :
noncomputable def finsupp.sum_finsupp_equiv_prod_finsupp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] :
β →₀ γ) →₀ γ) × →₀ γ)

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

This is the finsupp version of equiv.sum_arrow_equiv_prod_arrow.

Equations
theorem finsupp.fst_sum_finsupp_equiv_prod_finsupp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (f : α β →₀ γ) (x : α) :
theorem finsupp.snd_sum_finsupp_equiv_prod_finsupp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (f : α β →₀ γ) (y : β) :
theorem finsupp.sum_finsupp_equiv_prod_finsupp_symm_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (fg : →₀ γ) × →₀ γ)) (x : α) :
theorem finsupp.sum_finsupp_equiv_prod_finsupp_symm_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (fg : →₀ γ) × →₀ γ)) (y : β) :
noncomputable def finsupp.sum_finsupp_add_equiv_prod_finsupp {M : Type u_5} [add_monoid M] {α : Type u_1} {β : Type u_2} :
β →₀ M) ≃+ →₀ M) × →₀ M)

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

This is the finsupp version of equiv.sum_arrow_equiv_prod_arrow.

Equations
theorem finsupp.fst_sum_finsupp_add_equiv_prod_finsupp {M : Type u_5} [add_monoid M] {α : Type u_1} {β : Type u_2} (f : α β →₀ M) (x : α) :
theorem finsupp.snd_sum_finsupp_add_equiv_prod_finsupp {M : Type u_5} [add_monoid M] {α : Type u_1} {β : Type u_2} (f : α β →₀ M) (y : β) :
theorem finsupp.sum_finsupp_add_equiv_prod_finsupp_symm_inl {M : Type u_5} [add_monoid M] {α : Type u_1} {β : Type u_2} (fg : →₀ M) × →₀ M)) (x : α) :
theorem finsupp.sum_finsupp_add_equiv_prod_finsupp_symm_inr {M : Type u_5} [add_monoid M] {α : Type u_1} {β : Type u_2} (fg : →₀ M) × →₀ M)) (y : β) :

Declarations about scalar multiplication #

@[simp]
theorem finsupp.single_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} [has_zero M] [monoid_with_zero R] [mul_action_with_zero R M] (a b : α) (f : α M) (r : R) :
(finsupp.single a r) b f a = (finsupp.single a (r f b)) b
noncomputable def finsupp.comap_has_smul {α : Type u_1} {M : Type u_5} {G : Type u_9} [monoid G] [mul_action G α] [add_comm_monoid M] :
has_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
theorem finsupp.comap_smul_def {α : Type u_1} {M : Type u_5} {G : Type u_9} [monoid G] [mul_action G α] [add_comm_monoid M] (g : G) (f : α →₀ M) :
@[simp]
theorem finsupp.comap_smul_single {α : Type u_1} {M : Type u_5} {G : Type u_9} [monoid G] [mul_action G α] [add_comm_monoid M] (g : G) (a : α) (b : M) :
noncomputable def finsupp.comap_mul_action {α : Type u_1} {M : Type u_5} {G : Type u_9} [monoid G] [mul_action G α] [add_comm_monoid M] :

finsupp.comap_has_smul is multiplicative

Equations
noncomputable def finsupp.comap_distrib_mul_action {α : Type u_1} {M : Type u_5} {G : Type u_9} [monoid G] [mul_action G α] [add_comm_monoid M] :

finsupp.comap_has_smul is distributive

Equations
@[simp]
theorem finsupp.comap_smul_apply {α : Type u_1} {M : Type u_5} {G : Type u_9} [group G] [mul_action G α] [add_comm_monoid M] (g : G) (f : α →₀ M) (a : α) :
(g f) a = f (g⁻¹ a)

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

@[protected, instance]
noncomputable def finsupp.smul_zero_class {α : Type u_1} {M : Type u_5} {R : Type u_11} [has_zero M] [smul_zero_class R M] :
Equations

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} [has_zero M] [smul_zero_class 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} [has_zero M] [smul_zero_class R M] (b : R) (v : α →₀ M) (a : α) :
(b v) a = b v a
theorem is_smul_regular.finsupp {α : Type u_1} {M : Type u_5} {R : Type u_11} [has_zero M] [smul_zero_class R M] {k : R} (hk : is_smul_regular M k) :
@[protected, instance]
def finsupp.has_faithful_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} [nonempty α] [has_zero M] [smul_zero_class R M] [has_faithful_smul R M] :
@[protected, instance]
noncomputable def finsupp.distrib_smul (α : Type u_1) (M : Type u_5) {R : Type u_11} [add_zero_class M] [distrib_smul R M] :
Equations
@[protected, instance]
noncomputable def finsupp.distrib_mul_action (α : Type u_1) (M : Type u_5) {R : Type u_11} [monoid R] [add_monoid M] [distrib_mul_action R M] :
Equations
@[protected, instance]
def finsupp.is_scalar_tower (α : Type u_1) (M : Type u_5) {R : Type u_11} {S : Type u_12} [has_zero M] [smul_zero_class R M] [smul_zero_class S M] [has_smul R S] [is_scalar_tower R S M] :
@[protected, instance]
def finsupp.smul_comm_class (α : Type u_1) (M : Type u_5) {R : Type u_11} {S : Type u_12} [has_zero M] [smul_zero_class R M] [smul_zero_class S M] [smul_comm_class R S M] :
@[protected, instance]
@[protected, instance]
noncomputable def finsupp.module (α : Type u_1) (M : Type u_5) {R : Type u_11} [semiring R] [add_comm_monoid M] [module R M] :
module R →₀ M)
Equations
theorem finsupp.support_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} [add_monoid M] [smul_zero_class R M] {b : R} {g : α →₀ M} :
@[simp]
theorem finsupp.support_smul_eq {α : Type u_1} {M : Type u_5} {R : Type u_11} [semiring R] [add_comm_monoid M] [module R M] [no_zero_smul_divisors R M] {b : R} (hb : b 0) {g : α →₀ M} :
@[simp]
theorem finsupp.filter_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} {p : α Prop} {_x : monoid R} [add_monoid M] [distrib_mul_action R M] {b : R} {v : α →₀ M} :
theorem finsupp.map_domain_smul {α : Type u_1} {β : Type u_2} {M : Type u_5} {R : Type u_11} {_x : monoid R} [add_comm_monoid M] [distrib_mul_action R M] {f : α β} (b : R) (v : α →₀ M) :
@[simp]
theorem finsupp.smul_single {α : Type u_1} {M : Type u_5} {R : Type u_11} [has_zero M] [smul_zero_class R M] (c : R) (a : α) (b : M) :
@[simp]
theorem finsupp.smul_single' {α : Type u_1} {R : Type u_11} {_x : semiring R} (c : R) (a : α) (b : R) :
theorem finsupp.map_range_smul {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} {_x : monoid R} [add_monoid M] [distrib_mul_action R M] [add_monoid N] [distrib_mul_action R N] {f : M N} {hf : f 0 = 0} (c : R) (v : α →₀ M) (hsmul : (x : M), f (c x) = c f x) :
theorem finsupp.smul_single_one {α : Type u_1} {R : Type u_11} [semiring R] (a : α) (b : R) :
theorem finsupp.comap_domain_smul {α : Type u_1} {β : Type u_2} {M : Type u_5} {R : Type u_11} [add_monoid M] [monoid R] [distrib_mul_action R M] {f : α β} (r : R) (v : β →₀ M) (hfv : set.inj_on f (f ⁻¹' (v.support))) (hfrv : set.inj_on f (f ⁻¹' ((r v).support)) := _) :
theorem finsupp.comap_domain_smul_of_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} {R : Type u_11} [add_monoid M] [monoid R] [distrib_mul_action R M] {f : α β} (hf : function.injective f) (r : R) (v : β →₀ M) :

A version of finsupp.comap_domain_smul that's easier to use.

theorem finsupp.sum_smul_index {α : Type u_1} {M : Type u_5} {R : Type u_11} [semiring R] [add_comm_monoid M] {g : α →₀ R} {b : R} {h : α R M} (h0 : (i : α), h i 0 = 0) :
(b g).sum h = g.sum (λ (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} [add_monoid M] [distrib_smul R M] [add_comm_monoid N] {g : α →₀ M} {b : R} {h : α M N} (h0 : (i : α), h i 0 = 0) :
(b g).sum h = g.sum (λ (i : α) (c : M), h i (b c))
theorem finsupp.sum_smul_index_add_monoid_hom {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} [add_monoid M] [add_comm_monoid N] [distrib_smul R M] {g : α →₀ M} {b : R} {h : α M →+ N} :
(b g).sum (λ (a : α), (h a)) = g.sum (λ (i : α) (c : M), (h i) (b c))

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

@[protected, instance]
def finsupp.no_zero_smul_divisors {M : Type u_5} {R : Type u_11} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_1} [no_zero_smul_divisors R M] :
noncomputable def finsupp.distrib_mul_action_hom.single {α : Type u_1} {M : Type u_5} {R : Type u_11} [semiring R] [add_comm_monoid M] [distrib_mul_action R M] (a : α) :
M →+[R] α →₀ M

finsupp.single as a distrib_mul_action_hom.

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

Equations
theorem finsupp.distrib_mul_action_hom_ext {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} [semiring R] [add_comm_monoid M] [add_comm_monoid N] [distrib_mul_action R M] [distrib_mul_action R N] {f g : →₀ M) →+[R] N} (h : (a : α) (m : M), f (finsupp.single a m) = g (finsupp.single a m)) :
f = g
@[protected, instance]
def finsupp.unique_of_right {α : Type u_1} {R : Type u_11} [has_zero R] [subsingleton R] :
unique →₀ R)

The finsupp version of pi.unique.

Equations
@[protected, instance]
def finsupp.unique_of_left {α : Type u_1} {R : Type u_11} [has_zero R] [is_empty α] :
unique →₀ R)

The finsupp version of pi.unique_of_is_empty.

Equations
noncomputable def finsupp.restrict_support_equiv {α : Type u_1} (s : set α) (M : Type u_2) [add_comm_monoid M] :
{f // (f.support) s} (s →₀ M)

Given an add_comm_monoid M and s : set α, restrict_support_equiv 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
@[simp]
theorem finsupp.dom_congr_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (e : α β) (l : α →₀ M) :
@[protected]
def finsupp.dom_congr {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (e : α β) :
→₀ M) ≃+ →₀ M)

Given add_comm_monoid M and e : α ≃ β, dom_congr e is the corresponding equiv between α →₀ M and β →₀ M.

This is finsupp.equiv_congr_left as an add_equiv.

Equations
@[simp]
@[simp]
theorem finsupp.dom_congr_symm {α : Type u_1} {β : Type u_2} {M : Type u_5} [add_comm_monoid M] (e : α β) :
@[simp]
theorem finsupp.dom_congr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [add_comm_monoid M] (e : α β) (f : β γ) :

Declarations about sigma types #

noncomputable def finsupp.split {ι : Type u_4} {M : Type u_5} {αs : ι Type u_13} [has_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
theorem finsupp.split_apply {ι : Type u_4} {M : Type u_5} {αs : ι Type u_13} [has_zero M] (l : (Σ (i : ι), αs i) →₀ M) (i : ι) (x : αs i) :
(l.split i) x = l i, x⟩
noncomputable def finsupp.split_support {ι : Type u_4} {M : Type u_5} {αs : ι Type u_13} [has_zero M] (l : (Σ (i : ι), αs i) →₀ M) :

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

Equations
theorem finsupp.mem_split_support_iff_nonzero {ι : Type u_4} {M : Type u_5} {αs : ι Type u_13} [has_zero M] (l : (Σ (i : ι), αs i) →₀ M) (i : ι) :
noncomputable def finsupp.split_comp {ι : Type u_4} {M : Type u_5} {N : Type u_7} {αs : ι Type u_13} [has_zero M] (l : (Σ (i : ι), αs i) →₀ M) [has_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
theorem finsupp.sigma_support {ι : Type u_4} {M : Type u_5} {αs : ι Type u_13} [has_zero M] (l : (Σ (i : ι), αs i) →₀ M) :
l.support = l.split_support.sigma (λ (i : ι), (l.split i).support)
theorem finsupp.sigma_sum {ι : Type u_4} {M : Type u_5} {N : Type u_7} {αs : ι Type u_13} [has_zero M] (l : (Σ (i : ι), αs i) →₀ M) [add_comm_monoid N] (f : (Σ (i : ι), αs i) M N) :
l.sum f = l.split_support.sum (λ (i : ι), (l.split i).sum (λ (a : αs i) (b : M), f i, a⟩ b))
noncomputable def finsupp.sigma_finsupp_equiv_pi_finsupp {α : Type u_1} {η : Type u_14} [fintype η] {ιs : η Type u_15} [has_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
@[simp]
theorem finsupp.sigma_finsupp_equiv_pi_finsupp_apply {α : Type u_1} {η : Type u_14} [fintype η] {ιs : η Type u_15} [has_zero α] (f : (Σ (j : η), ιs j) →₀ α) (j : η) (i : ιs j) :
noncomputable def finsupp.sigma_finsupp_add_equiv_pi_finsupp {η : Type u_14} [fintype η] {α : Type u_1} {ιs : η Type u_2} [add_monoid α] :
((Σ (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 add_equiv version of finsupp.sigma_finsupp_equiv_pi_finsupp.

Equations
@[simp]
theorem finsupp.sigma_finsupp_add_equiv_pi_finsupp_apply {η : Type u_14} [fintype η] {α : Type u_1} {ιs : η Type u_2} [add_monoid α] (f : (Σ (j : η), ιs j) →₀ α) (j : η) (i : ιs j) :

Meta declarations #

@[protected, instance]
meta def finsupp.has_repr (ι : Type u_1) (α : Type u_2) [has_zero α] [has_repr ι] [has_repr α] :

Stringify a finsupp as a sequence of finsupp.single terms.

Note this is meta as it has to choose some order for the terms.