mathlib documentation

data.dfinsupp

Dependent functions with finite support

For a non-dependent version see data/finsupp.lean.

structure dfinsupp.pre (ι : Type u) (β : ι → Type v) [Π (i : ι), has_zero (β i)] :
Type (max u v)

@[instance]
def dfinsupp.inhabited_pre (ι : Type u) (β : ι → Type v) [Π (i : ι), has_zero (β i)] :

Equations
@[instance]
def dfinsupp.setoid (ι : Type u) (β : ι → Type v) [Π (i : ι), has_zero (β i)] :

Equations
def dfinsupp {ι : Type u} (β : ι → Type v) [Π (i : ι), has_zero (β i)] :
Type (max u v)

A dependent function Π i, β i with finite support.

Equations
@[instance]
def dfinsupp.has_coe_to_fun {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] :
has_coe_to_fun (Π₀ (i : ι), β i)

Equations
@[instance]
def dfinsupp.has_zero {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] :
has_zero (Π₀ (i : ι), β i)

Equations
@[instance]
def dfinsupp.inhabited {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] :
inhabited (Π₀ (i : ι), β i)

Equations
@[simp]
theorem dfinsupp.zero_apply {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] (i : ι) :
0 i = 0

@[ext]
theorem dfinsupp.ext {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] {f g : Π₀ (i : ι), β i} :
(∀ (i : ι), f i = g i)f = g

def dfinsupp.map_range {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), has_zero (β₁ i)] [Π (i : ι), has_zero (β₂ i)] (f : Π (i : ι), β₁ iβ₂ i) :
(∀ (i : ι), f i 0 = 0)(Π₀ (i : ι), β₁ i)(Π₀ (i : ι), β₂ i)

The composition of f : β₁ → β₂ and g : Π₀ i, β₁ i is map_range f hf g : Π₀ i, β₂ i, well defined when f 0 = 0.

Equations
@[simp]
theorem dfinsupp.map_range_apply {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), has_zero (β₁ i)] [Π (i : ι), has_zero (β₂ i)] (f : Π (i : ι), β₁ iβ₂ i) (hf : ∀ (i : ι), f i 0 = 0) (g : Π₀ (i : ι), β₁ i) (i : ι) :
(dfinsupp.map_range f hf g) i = f i (g i)

def dfinsupp.zip_with {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), has_zero (β₁ i)] [Π (i : ι), has_zero (β₂ i)] (f : Π (i : ι), β₁ iβ₂ iβ i) :
(∀ (i : ι), f i 0 0 = 0)(Π₀ (i : ι), β₁ i)(Π₀ (i : ι), β₂ i)(Π₀ (i : ι), β i)

Let f i be a binary operation β₁ i → β₂ i → β i such that f i 0 0 = 0. Then zip_with f hf is a binary operation Π₀ i, β₁ i → Π₀ i, β₂ i → Π₀ i, β i.

Equations
@[simp]
theorem dfinsupp.zip_with_apply {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), has_zero (β₁ i)] [Π (i : ι), has_zero (β₂ i)] (f : Π (i : ι), β₁ iβ₂ iβ i) (hf : ∀ (i : ι), f i 0 0 = 0) (g₁ : Π₀ (i : ι), β₁ i) (g₂ : Π₀ (i : ι), β₂ i) (i : ι) :
(dfinsupp.zip_with f hf g₁ g₂) i = f i (g₁ i) (g₂ i)

@[instance]
def dfinsupp.has_add {ι : Type u} {β : ι → Type v} [Π (i : ι), add_monoid (β i)] :
has_add (Π₀ (i : ι), β i)

Equations
@[simp]
theorem dfinsupp.add_apply {ι : Type u} {β : ι → Type v} [Π (i : ι), add_monoid (β i)] (g₁ g₂ : Π₀ (i : ι), β i) (i : ι) :
(g₁ + g₂) i = g₁ i + g₂ i

@[instance]
def dfinsupp.add_monoid {ι : Type u} {β : ι → Type v} [Π (i : ι), add_monoid (β i)] :
add_monoid (Π₀ (i : ι), β i)

Equations
@[instance]
def dfinsupp.is_add_monoid_hom {ι : Type u} {β : ι → Type v} [Π (i : ι), add_monoid (β i)] {i : ι} :
is_add_monoid_hom (λ (g : Π₀ (i : ι), β i), g i)

@[instance]
def dfinsupp.has_neg {ι : Type u} {β : ι → Type v} [Π (i : ι), add_group (β i)] :
has_neg (Π₀ (i : ι), β i)

Equations
@[instance]
def dfinsupp.add_comm_monoid {ι : Type u} {β : ι → Type v} [Π (i : ι), add_comm_monoid (β i)] :
add_comm_monoid (Π₀ (i : ι), β i)

Equations
@[simp]
theorem dfinsupp.neg_apply {ι : Type u} {β : ι → Type v} [Π (i : ι), add_group (β i)] (g : Π₀ (i : ι), β i) (i : ι) :
(-g) i = -g i

@[instance]
def dfinsupp.add_group {ι : Type u} {β : ι → Type v} [Π (i : ι), add_group (β i)] :
add_group (Π₀ (i : ι), β i)

Equations
@[simp]
theorem dfinsupp.sub_apply {ι : Type u} {β : ι → Type v} [Π (i : ι), add_group (β i)] (g₁ g₂ : Π₀ (i : ι), β i) (i : ι) :
(g₁ - g₂) i = g₁ i - g₂ i

@[instance]
def dfinsupp.add_comm_group {ι : Type u} {β : ι → Type v} [Π (i : ι), add_comm_group (β i)] :
add_comm_group (Π₀ (i : ι), β i)

Equations
def dfinsupp.to_has_scalar {ι : Type u} {β : ι → Type v} {γ : Type w} [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), semimodule γ (β i)] :
has_scalar γ (Π₀ (i : ι), β i)

Dependent functions with finite support inherit a semiring action from an action on each coordinate.

Equations
@[simp]
theorem dfinsupp.smul_apply {ι : Type u} {β : ι → Type v} {γ : Type w} [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), semimodule γ (β i)] (b : γ) (v : Π₀ (i : ι), β i) (i : ι) :
(b v) i = b v i

def dfinsupp.to_semimodule {ι : Type u} {β : ι → Type v} {γ : Type w} [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), semimodule γ (β i)] :
semimodule γ (Π₀ (i : ι), β i)

Dependent functions with finite support inherit a semimodule structure from such a structure on each coordinate.

Equations
def dfinsupp.filter {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] (p : ι → Prop) [decidable_pred p] :
(Π₀ (i : ι), β i)(Π₀ (i : ι), β i)

filter p f is the function which is f i if p i is true and 0 otherwise.

Equations
@[simp]
theorem dfinsupp.filter_apply {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] (p : ι → Prop) [decidable_pred p] (i : ι) (f : Π₀ (i : ι), β i) :
(dfinsupp.filter p f) i = ite (p i) (f i) 0

theorem dfinsupp.filter_apply_pos {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] {p : ι → Prop} [decidable_pred p] (f : Π₀ (i : ι), β i) {i : ι} :
p i(dfinsupp.filter p f) i = f i

theorem dfinsupp.filter_apply_neg {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] {p : ι → Prop} [decidable_pred p] (f : Π₀ (i : ι), β i) {i : ι} :
¬p i(dfinsupp.filter p f) i = 0

theorem dfinsupp.filter_pos_add_filter_neg {ι : Type u} {β : ι → Type v} [Π (i : ι), add_monoid (β i)] (f : Π₀ (i : ι), β i) (p : ι → Prop) [decidable_pred p] :
dfinsupp.filter p f + dfinsupp.filter (λ (i : ι), ¬p i) f = f

def dfinsupp.subtype_domain {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] (p : ι → Prop) [decidable_pred p] :
(Π₀ (i : ι), β i)(Π₀ (i : subtype p), β i)

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

Equations
@[simp]
theorem dfinsupp.subtype_domain_zero {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] {p : ι → Prop} [decidable_pred p] :

@[simp]
theorem dfinsupp.subtype_domain_apply {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] {p : ι → Prop} [decidable_pred p] {i : subtype p} {v : Π₀ (i : ι), β i} :

@[simp]
theorem dfinsupp.subtype_domain_add {ι : Type u} {β : ι → Type v} [Π (i : ι), add_monoid (β i)] {p : ι → Prop} [decidable_pred p] {v v' : Π₀ (i : ι), β i} :

@[instance]
def dfinsupp.subtype_domain.is_add_monoid_hom {ι : Type u} {β : ι → Type v} [Π (i : ι), add_monoid (β i)] {p : ι → Prop} [decidable_pred p] :

@[simp]
theorem dfinsupp.subtype_domain_neg {ι : Type u} {β : ι → Type v} [Π (i : ι), add_group (β i)] {p : ι → Prop} [decidable_pred p] {v : Π₀ (i : ι), β i} :

@[simp]
theorem dfinsupp.subtype_domain_sub {ι : Type u} {β : ι → Type v} [Π (i : ι), add_group (β i)] {p : ι → Prop} [decidable_pred p] {v v' : Π₀ (i : ι), β i} :

theorem dfinsupp.finite_supp {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] (f : Π₀ (i : ι), β i) :
{i : ι | f i 0}.finite

def dfinsupp.mk {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] (s : finset ι) :
(Π (i : s), β i)(Π₀ (i : ι), β i)

Create an element of Π₀ i, β i from a finset s and a function x defined on this finset.

Equations
@[simp]
theorem dfinsupp.mk_apply {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {s : finset ι} {x : Π (i : s), β i} {i : ι} :
(dfinsupp.mk s x) i = dite (i s) (λ (H : i s), x i, H⟩) (λ (H : i s), 0)

theorem dfinsupp.mk_injective {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] (s : finset ι) :

def dfinsupp.single {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] (i : ι) :
β i(Π₀ (i : ι), β i)

The function single i b : Π₀ i, β i sends i to b and all other points to 0.

Equations
@[simp]
theorem dfinsupp.single_apply {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i i' : ι} {b : β i} :
(dfinsupp.single i b) i' = dite (i = i') (λ (h : i = i'), h.rec_on b) (λ (h : ¬i = i'), 0)

@[simp]
theorem dfinsupp.single_zero {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i : ι} :

@[simp]
theorem dfinsupp.single_eq_same {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i : ι} {b : β i} :

theorem dfinsupp.single_eq_of_ne {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i i' : ι} {b : β i} :
i i'(dfinsupp.single i b) i' = 0

theorem dfinsupp.single_injective {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i : ι} :

def dfinsupp.erase {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] :
ι → (Π₀ (i : ι), β i)(Π₀ (i : ι), β i)

Redefine f i to be 0.

Equations
@[simp]
theorem dfinsupp.erase_apply {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i j : ι} {f : Π₀ (i : ι), β i} :
(dfinsupp.erase i f) j = ite (j = i) 0 (f j)

@[simp]
theorem dfinsupp.erase_same {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i : ι} {f : Π₀ (i : ι), β i} :

theorem dfinsupp.erase_ne {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i i' : ι} {f : Π₀ (i : ι), β i} :
i' i(dfinsupp.erase i f) i' = f i'

@[simp]
theorem dfinsupp.single_add {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_monoid (β i)] {i : ι} {b₁ b₂ : β i} :
dfinsupp.single i (b₁ + b₂) = dfinsupp.single i b₁ + dfinsupp.single i b₂

theorem dfinsupp.single_add_erase {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_monoid (β i)] {i : ι} {f : Π₀ (i : ι), β i} :

theorem dfinsupp.erase_add_single {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_monoid (β i)] {i : ι} {f : Π₀ (i : ι), β i} :

theorem dfinsupp.induction {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_monoid (β i)] {p : (Π₀ (i : ι), β i) → Prop} (f : Π₀ (i : ι), β i) :
p 0(∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0b 0p fp (dfinsupp.single i b + f))p f

theorem dfinsupp.induction₂ {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_monoid (β i)] {p : (Π₀ (i : ι), β i) → Prop} (f : Π₀ (i : ι), β i) :
p 0(∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0b 0p fp (f + dfinsupp.single i b))p f

@[simp]
theorem dfinsupp.mk_add {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_monoid (β i)] {s : finset ι} {x y : Π (i : s), β i} :

@[simp]
theorem dfinsupp.mk_zero {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {s : finset ι} :

@[simp]
theorem dfinsupp.mk_neg {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_group (β i)] {s : finset ι} {x : Π (i : s), β i.val} :

@[simp]
theorem dfinsupp.mk_sub {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_group (β i)] {s : finset ι} {x y : Π (i : s), β i.val} :

@[instance]
def dfinsupp.is_add_group_hom {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_group (β i)] {s : finset ι} :

@[simp]
theorem dfinsupp.mk_smul {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] (γ : Type w) [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), semimodule γ (β i)] {s : finset ι} {c : γ} (x : Π (i : s), β i.val) :

@[simp]
theorem dfinsupp.single_smul {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] (γ : Type w) [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), semimodule γ (β i)] {i : ι} {c : γ} {x : β i} :

def dfinsupp.lmk {ι : Type u} (β : ι → Type v) [dec : decidable_eq ι] (γ : Type w) [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), semimodule γ (β i)] (s : finset ι) :
(Π (i : s), β i.val) →ₗ[γ] Π₀ (i : ι), β i

dfinsupp.mk as a linear_map.

Equations
def dfinsupp.lsingle {ι : Type u} (β : ι → Type v) [dec : decidable_eq ι] (γ : Type w) [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), semimodule γ (β i)] (i : ι) :
β i →ₗ[γ] Π₀ (i : ι), β i

dfinsupp.single as a linear_map

Equations
@[simp]
theorem dfinsupp.lmk_apply {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] (γ : Type w) [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), semimodule γ (β i)] {s : finset ι} {x : Π (i : s), β i.val} :
(dfinsupp.lmk β γ s) x = dfinsupp.mk s x

@[simp]
theorem dfinsupp.lsingle_apply {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] (γ : Type w) [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), semimodule γ (β i)] {i : ι} {x : β i} :

def dfinsupp.support {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] :
(Π₀ (i : ι), β i)finset ι

Set {i | f x ≠ 0} as a finset.

Equations
@[simp]
theorem dfinsupp.support_mk_subset {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {s : finset ι} {x : Π (i : s), β i.val} :

@[simp]
theorem dfinsupp.mem_support_to_fun {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] (f : Π₀ (i : ι), β i) (i : ι) :
i f.support f i 0

theorem dfinsupp.eq_mk_support {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] (f : Π₀ (i : ι), β i) :
f = dfinsupp.mk f.support (λ (i : (f.support)), f i)

@[simp]
theorem dfinsupp.support_zero {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] :

theorem dfinsupp.mem_support_iff {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] (f : Π₀ (i : ι), β i) (i : ι) :
i f.support f i 0

@[simp]
theorem dfinsupp.support_eq_empty {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {f : Π₀ (i : ι), β i} :
f.support = f = 0

@[instance]
def dfinsupp.decidable_zero {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] :

Equations
theorem dfinsupp.support_subset_iff {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {s : set ι} {f : Π₀ (i : ι), β i} :
(f.support) s ∀ (i : ι), i sf i = 0

theorem dfinsupp.support_single_ne_zero {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {i : ι} {b : β i} :
b 0(dfinsupp.single i b).support = {i}

theorem dfinsupp.support_single_subset {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {i : ι} {b : β i} :

theorem dfinsupp.map_range_def {ι : Type u} [dec : decidable_eq ι] {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), has_zero (β₁ i)] [Π (i : ι), has_zero (β₂ i)] [Π (i : ι) (x : β₁ i), decidable (x 0)] {f : Π (i : ι), β₁ iβ₂ i} {hf : ∀ (i : ι), f i 0 = 0} {g : Π₀ (i : ι), β₁ i} :
dfinsupp.map_range f hf g = dfinsupp.mk g.support (λ (i : (g.support)), f i.val (g i.val))

@[simp]
theorem dfinsupp.map_range_single {ι : Type u} [dec : decidable_eq ι] {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), has_zero (β₁ i)] [Π (i : ι), has_zero (β₂ i)] {f : Π (i : ι), β₁ iβ₂ i} {hf : ∀ (i : ι), f i 0 = 0} {i : ι} {b : β₁ i} :

theorem dfinsupp.support_map_range {ι : Type u} [dec : decidable_eq ι] {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), has_zero (β₁ i)] [Π (i : ι), has_zero (β₂ i)] [Π (i : ι) (x : β₁ i), decidable (x 0)] [Π (i : ι) (x : β₂ i), decidable (x 0)] {f : Π (i : ι), β₁ iβ₂ i} {hf : ∀ (i : ι), f i 0 = 0} {g : Π₀ (i : ι), β₁ i} :

theorem dfinsupp.zip_with_def {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), has_zero (β₁ i)] [Π (i : ι), has_zero (β₂ i)] [Π (i : ι) (x : β₁ i), decidable (x 0)] [Π (i : ι) (x : β₂ i), decidable (x 0)] {f : Π (i : ι), β₁ iβ₂ iβ i} {hf : ∀ (i : ι), f i 0 0 = 0} {g₁ : Π₀ (i : ι), β₁ i} {g₂ : Π₀ (i : ι), β₂ i} :
dfinsupp.zip_with f hf g₁ g₂ = dfinsupp.mk (g₁.support g₂.support) (λ (i : (g₁.support g₂.support)), f i.val (g₁ i.val) (g₂ i.val))

theorem dfinsupp.support_zip_with {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), has_zero (β₁ i)] [Π (i : ι), has_zero (β₂ i)] [Π (i : ι) (x : β₁ i), decidable (x 0)] [Π (i : ι) (x : β₂ i), decidable (x 0)] {f : Π (i : ι), β₁ iβ₂ iβ i} {hf : ∀ (i : ι), f i 0 0 = 0} {g₁ : Π₀ (i : ι), β₁ i} {g₂ : Π₀ (i : ι), β₂ i} :
(dfinsupp.zip_with f hf g₁ g₂).support g₁.support g₂.support

theorem dfinsupp.erase_def {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] (i : ι) (f : Π₀ (i : ι), β i) :

@[simp]
theorem dfinsupp.support_erase {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] (i : ι) (f : Π₀ (i : ι), β i) :

theorem dfinsupp.filter_def {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {p : ι → Prop} [decidable_pred p] (f : Π₀ (i : ι), β i) :

@[simp]
theorem dfinsupp.support_filter {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {p : ι → Prop} [decidable_pred p] (f : Π₀ (i : ι), β i) :

theorem dfinsupp.subtype_domain_def {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {p : ι → Prop} [decidable_pred p] (f : Π₀ (i : ι), β i) :

@[simp]
theorem dfinsupp.support_subtype_domain {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {p : ι → Prop} [decidable_pred p] {f : Π₀ (i : ι), β i} :

theorem dfinsupp.support_add {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {g₁ g₂ : Π₀ (i : ι), β i} :
(g₁ + g₂).support g₁.support g₂.support

@[simp]
theorem dfinsupp.support_neg {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_group (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {f : Π₀ (i : ι), β i} :

theorem dfinsupp.support_smul {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), semimodule γ (β i)] [Π (i : ι) (x : β i), decidable (x 0)] (b : γ) (v : Π₀ (i : ι), β i) :

@[instance]
def dfinsupp.decidable_eq {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι), decidable_eq (β i)] :
decidable_eq (Π₀ (i : ι), β i)

Equations
def dfinsupp.sum {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [add_comm_monoid γ] :
(Π₀ (i : ι), β i)(Π (i : ι), β i → γ) → γ

sum f g is the sum of g i (f i) over the support of f.

Equations
def dfinsupp.prod {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [comm_monoid γ] :
(Π₀ (i : ι), β i)(Π (i : ι), β i → γ) → γ

prod f g is the product of g i (f i) over the support of f.

Equations
theorem dfinsupp.sum_map_range_index {ι : Type u} [dec : decidable_eq ι] {γ : Type w} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), has_zero (β₁ i)] [Π (i : ι), has_zero (β₂ i)] [Π (i : ι) (x : β₁ i), decidable (x 0)] [Π (i : ι) (x : β₂ i), decidable (x 0)] [add_comm_monoid γ] {f : Π (i : ι), β₁ iβ₂ i} {hf : ∀ (i : ι), f i 0 = 0} {g : Π₀ (i : ι), β₁ i} {h : Π (i : ι), β₂ i → γ} :
(∀ (i : ι), h i 0 = 0)(dfinsupp.map_range f hf g).sum h = g.sum (λ (i : ι) (b : β₁ i), h i (f i b))

theorem dfinsupp.prod_map_range_index {ι : Type u} [dec : decidable_eq ι] {γ : Type w} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), has_zero (β₁ i)] [Π (i : ι), has_zero (β₂ i)] [Π (i : ι) (x : β₁ i), decidable (x 0)] [Π (i : ι) (x : β₂ i), decidable (x 0)] [comm_monoid γ] {f : Π (i : ι), β₁ iβ₂ i} {hf : ∀ (i : ι), f i 0 = 0} {g : Π₀ (i : ι), β₁ i} {h : Π (i : ι), β₂ i → γ} :
(∀ (i : ι), h i 0 = 1)(dfinsupp.map_range f hf g).prod h = g.prod (λ (i : ι) (b : β₁ i), h i (f i b))

theorem dfinsupp.prod_zero_index {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [comm_monoid γ] {h : Π (i : ι), β i → γ} :
0.prod h = 1

theorem dfinsupp.sum_zero_index {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [add_comm_monoid γ] {h : Π (i : ι), β i → γ} :
0.sum h = 0

theorem dfinsupp.prod_single_index {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [comm_monoid γ] {i : ι} {b : β i} {h : Π (i : ι), β i → γ} :
h i 0 = 1(dfinsupp.single i b).prod h = h i b

theorem dfinsupp.sum_single_index {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [add_comm_monoid γ] {i : ι} {b : β i} {h : Π (i : ι), β i → γ} :
h i 0 = 0(dfinsupp.single i b).sum h = h i b

theorem dfinsupp.prod_neg_index {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_group (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [comm_monoid γ] {g : Π₀ (i : ι), β i} {h : Π (i : ι), β i → γ} :
(∀ (i : ι), h i 0 = 1)(-g).prod h = g.prod (λ (i : ι) (b : β i), h i (-b))

theorem dfinsupp.sum_neg_index {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_group (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [add_comm_monoid γ] {g : Π₀ (i : ι), β i} {h : Π (i : ι), β i → γ} :
(∀ (i : ι), h i 0 = 0)(-g).sum h = g.sum (λ (i : ι) (b : β i), h i (-b))

@[simp]
theorem dfinsupp.sum_apply {ι : Type u} {β : ι → Type v} {ι₁ : Type u₁} [decidable_eq ι₁] {β₁ : ι₁ → Type v₁} [Π (i₁ : ι₁), has_zero (β₁ i₁)] [Π (i : ι₁) (x : β₁ i), decidable (x 0)] [Π (i : ι), add_comm_monoid (β i)] {f : Π₀ (i₁ : ι₁), β₁ i₁} {g : Π (i₁ : ι₁), β₁ i₁(Π₀ (i : ι), β i)} {i₂ : ι} :
(f.sum g) i₂ = f.sum (λ (i₁ : ι₁) (b : β₁ i₁), (g i₁ b) i₂)

theorem dfinsupp.support_sum {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {ι₁ : Type u₁} [decidable_eq ι₁] {β₁ : ι₁ → Type v₁} [Π (i₁ : ι₁), has_zero (β₁ i₁)] [Π (i : ι₁) (x : β₁ i), decidable (x 0)] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {f : Π₀ (i₁ : ι₁), β₁ i₁} {g : Π (i₁ : ι₁), β₁ i₁(Π₀ (i : ι), β i)} :
(f.sum g).support f.support.bind (λ (i : ι₁), (g i (f i)).support)

@[simp]
theorem dfinsupp.prod_one {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [comm_monoid γ] {f : Π₀ (i : ι), β i} :
f.prod (λ (i : ι) (b : β i), 1) = 1

@[simp]
theorem dfinsupp.sum_zero {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [add_comm_monoid γ] {f : Π₀ (i : ι), β i} :
f.sum (λ (i : ι) (b : β i), 0) = 0

@[simp]
theorem dfinsupp.sum_add {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [add_comm_monoid γ] {f : Π₀ (i : ι), β i} {h₁ h₂ : Π (i : ι), β i → γ} :
f.sum (λ (i : ι) (b : β i), h₁ i b + h₂ i b) = f.sum h₁ + f.sum h₂

@[simp]
theorem dfinsupp.prod_mul {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [comm_monoid γ] {f : Π₀ (i : ι), β i} {h₁ h₂ : Π (i : ι), β i → γ} :
f.prod (λ (i : ι) (b : β i), (h₁ i b) * h₂ i b) = (f.prod h₁) * f.prod h₂

@[simp]
theorem dfinsupp.sum_neg {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [add_comm_group γ] {f : Π₀ (i : ι), β i} {h : Π (i : ι), β i → γ} :
f.sum (λ (i : ι) (b : β i), -h i b) = -f.sum h

@[simp]
theorem dfinsupp.prod_inv {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [comm_group γ] {f : Π₀ (i : ι), β i} {h : Π (i : ι), β i → γ} :
f.prod (λ (i : ι) (b : β i), (h i b)⁻¹) = (f.prod h)⁻¹

theorem dfinsupp.sum_add_index {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [add_comm_monoid γ] {f g : Π₀ (i : ι), β i} {h : Π (i : ι), β i → γ} :
(∀ (i : ι), h i 0 = 0)(∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ + h i b₂)(f + g).sum h = f.sum h + g.sum h

theorem dfinsupp.prod_add_index {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [comm_monoid γ] {f g : Π₀ (i : ι), β i} {h : Π (i : ι), β i → γ} :
(∀ (i : ι), h i 0 = 1)(∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = (h i b₁) * h i b₂)(f + g).prod h = (f.prod h) * g.prod h

theorem dfinsupp.sum_sub_index {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_comm_group (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [add_comm_group γ] {f g : Π₀ (i : ι), β i} {h : Π (i : ι), β i → γ} :
(∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂)(f - g).sum h = f.sum h - g.sum h

theorem dfinsupp.prod_finset_sum_index {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} {α : Type x} [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [comm_monoid γ] {s : finset α} {g : α → (Π₀ (i : ι), β i)} {h : Π (i : ι), β i → γ} :
(∀ (i : ι), h i 0 = 1)(∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = (h i b₁) * h i b₂)∏ (i : α) in s, (g i).prod h = (∑ (i : α) in s, g i).prod h

theorem dfinsupp.sum_finset_sum_index {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} {α : Type x} [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [add_comm_monoid γ] {s : finset α} {g : α → (Π₀ (i : ι), β i)} {h : Π (i : ι), β i → γ} :
(∀ (i : ι), h i 0 = 0)(∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ + h i b₂)∑ (i : α) in s, (g i).sum h = (∑ (i : α) in s, g i).sum h

theorem dfinsupp.sum_sum_index {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} {ι₁ : Type u₁} [decidable_eq ι₁] {β₁ : ι₁ → Type v₁} [Π (i₁ : ι₁), has_zero (β₁ i₁)] [Π (i : ι₁) (x : β₁ i), decidable (x 0)] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [add_comm_monoid γ] {f : Π₀ (i₁ : ι₁), β₁ i₁} {g : Π (i₁ : ι₁), β₁ i₁(Π₀ (i : ι), β i)} {h : Π (i : ι), β i → γ} :
(∀ (i : ι), h i 0 = 0)(∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ + h i b₂)(f.sum g).sum h = f.sum (λ (i : ι₁) (b : β₁ i), (g i b).sum h)

theorem dfinsupp.prod_sum_index {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} {ι₁ : Type u₁} [decidable_eq ι₁] {β₁ : ι₁ → Type v₁} [Π (i₁ : ι₁), has_zero (β₁ i₁)] [Π (i : ι₁) (x : β₁ i), decidable (x 0)] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [comm_monoid γ] {f : Π₀ (i₁ : ι₁), β₁ i₁} {g : Π (i₁ : ι₁), β₁ i₁(Π₀ (i : ι), β i)} {h : Π (i : ι), β i → γ} :
(∀ (i : ι), h i 0 = 1)(∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = (h i b₁) * h i b₂)(f.sum g).prod h = f.prod (λ (i : ι₁) (b : β₁ i), (g i b).prod h)

@[simp]
theorem dfinsupp.sum_single {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {f : Π₀ (i : ι), β i} :

theorem dfinsupp.sum_subtype_domain_index {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [add_comm_monoid γ] {v : Π₀ (i : ι), β i} {p : ι → Prop} [decidable_pred p] {h : Π (i : ι), β i → γ} :
(∀ (x : ι), x v.supportp x)(dfinsupp.subtype_domain p v).sum (λ (i : subtype p) (b : β i), h i b) = v.sum h

theorem dfinsupp.prod_subtype_domain_index {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] [comm_monoid γ] {v : Π₀ (i : ι), β i} {p : ι → Prop} [decidable_pred p] {h : Π (i : ι), β i → γ} :
(∀ (x : ι), x v.supportp x)(dfinsupp.subtype_domain p v).prod (λ (i : subtype p) (b : β i), h i b) = v.prod h

theorem dfinsupp.subtype_domain_sum {ι : Type u} {β : ι → Type v} {γ : Type w} [Π (i : ι), add_comm_monoid (β i)] {s : finset γ} {h : γ → (Π₀ (i : ι), β i)} {p : ι → Prop} [decidable_pred p] :
dfinsupp.subtype_domain p (∑ (c : γ) in s, h c) = ∑ (c : γ) in s, dfinsupp.subtype_domain p (h c)

theorem dfinsupp.subtype_domain_finsupp_sum {ι : Type u} {β : ι → Type v} {γ : Type w} {δ : γ → Type x} [decidable_eq γ] [Π (c : γ), has_zero (δ c)] [Π (c : γ) (x : δ c), decidable (x 0)] [Π (i : ι), add_comm_monoid (β i)] {p : ι → Prop} [decidable_pred p] {s : Π₀ (c : γ), δ c} {h : Π (c : γ), δ c(Π₀ (i : ι), β i)} :
dfinsupp.subtype_domain p (s.sum h) = s.sum (λ (c : γ) (d : δ c), dfinsupp.subtype_domain p (h c d))