mathlib documentation

data.dfinsupp

Dependent functions with finite support #

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

source
structure dfinsupp.pre (ι : Type u) (β : ι → Type v) [Π (i : ι), has_zero (β i)] :
Type (max u v)
source
@[protected, instance]
def dfinsupp.inhabited_pre (ι : Type u) (β : ι → Type v) [Π (i : ι), has_zero (β i)] :
inhabited (dfinsupp.pre ι β)
Equations
source
@[protected, instance]
def dfinsupp.pre.setoid (ι : Type u) (β : ι → Type v) [Π (i : ι), has_zero (β i)] :
setoid (dfinsupp.pre ι β)
Equations
source
def dfinsupp {ι : Type u} (β : ι → Type v) [Π (i : ι), has_zero (β i)] :
Type (max u v)

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

Equations
source
@[protected, instance]
def dfinsupp.has_coe_to_fun {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] :
has_coe_to_fun (Π₀ (i : ι), β i)
Equations
source
@[protected, instance]
def dfinsupp.has_zero {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] :
has_zero (Π₀ (i : ι), β i)
Equations
source
@[protected, instance]
def dfinsupp.inhabited {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] :
inhabited (Π₀ (i : ι), β i)
Equations
source
@[simp]
theorem dfinsupp.coe_zero {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] :
⇑0 = 0
source
theorem dfinsupp.zero_apply {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] (i : ι) :
⇑0 i = 0
source
theorem dfinsupp.coe_fn_injective {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] :
function.injective coe_fn
source
@[ext]
theorem dfinsupp.ext {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] {f g : Π₀ (i : ι), β i} (H : ∀ (i : ι), ⇑f i = ⇑g i) :
f = g
source
def dfinsupp.map_range {ι : 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 : ι), β₂ i

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

This preserves the structure on f, and exists in various bundled forms for when f is itself bundled:

Equations
source
@[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)
source
@[simp]
theorem dfinsupp.map_range_id {ι : Type u} {β₁ : ι → Type v₁} [Π (i : ι), has_zero (β₁ i)] (h : (∀ (i : ι), id 0 = 0) := _) (g : Π₀ (i : ι), β₁ i) :
dfinsupp.map_range (λ (i : ι), id) h g = g
source
theorem dfinsupp.map_range_comp {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), has_zero (β i)] [Π (i : ι), has_zero (β₁ i)] [Π (i : ι), has_zero (β₂ i)] (f : Π (i : ι), β₁ i → β₂ i) (f₂ : Π (i : ι), β i → β₁ i) (hf : ∀ (i : ι), f i 0 = 0) (hf₂ : ∀ (i : ι), f₂ i 0 = 0) (h : ∀ (i : ι), (f i ∘ f₂ i) 0 = 0) (g : Π₀ (i : ι), β i) :
dfinsupp.map_range (λ (i : ι), f i ∘ f₂ i) h g = dfinsupp.map_range f hf (dfinsupp.map_range f₂ hf₂ g)
source
@[simp]
theorem dfinsupp.map_range_zero {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), has_zero (β₁ i)] [Π (i : ι), has_zero (β₂ i)] (f : Π (i : ι), β₁ i → β₂ i) (hf : ∀ (i : ι), f i 0 = 0) :
dfinsupp.map_range f hf 0 = 0
source
def dfinsupp.zip_with {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), has_zero (β i)] [Π (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 : ι), β 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
source
@[simp]
theorem dfinsupp.zip_with_apply {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), has_zero (β i)] [Π (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)
source
@[protected, instance]
def dfinsupp.has_add {ι : Type u} {β : ι → Type v} [Π (i : ι), add_zero_class (β i)] :
has_add (Π₀ (i : ι), β i)
Equations
source
theorem dfinsupp.add_apply {ι : Type u} {β : ι → Type v} [Π (i : ι), add_zero_class (β i)] (g₁ g₂ : Π₀ (i : ι), β i) (i : ι) :
⇑(g₁ + g₂) i = ⇑g₁ i + ⇑g₂ i
source
@[simp]
theorem dfinsupp.coe_add {ι : Type u} {β : ι → Type v} [Π (i : ι), add_zero_class (β i)] (g₁ g₂ : Π₀ (i : ι), β i) :
⇑(g₁ + g₂) = ⇑g₁ + ⇑g₂
source
@[protected, instance]
def dfinsupp.add_zero_class {ι : Type u} {β : ι → Type v} [Π (i : ι), add_zero_class (β i)] :
add_zero_class (Π₀ (i : ι), β i)
Equations
source
@[protected, instance]
def dfinsupp.add_monoid {ι : Type u} {β : ι → Type v} [Π (i : ι), add_monoid (β i)] :
add_monoid (Π₀ (i : ι), β i)
Equations
source
def dfinsupp.coe_fn_add_monoid_hom {ι : Type u} {β : ι → Type v} [Π (i : ι), add_zero_class (β i)] :
(Π₀ (i : ι), β i) →+ Π (i : ι), β i

Coercion from a dfinsupp to a pi type is an add_monoid_hom.

Equations
source
def dfinsupp.eval_add_monoid_hom {ι : Type u} {β : ι → Type v} [Π (i : ι), add_zero_class (β i)] (i : ι) :
(Π₀ (i : ι), β i) →+ β i

Evaluation at a point is an add_monoid_hom. This is the finitely-supported version of add_monoid_hom.apply.

Equations
source
@[protected, instance]
def dfinsupp.is_add_monoid_hom {ι : Type u} {β : ι → Type v} [Π (i : ι), add_zero_class (β i)] {i : ι} :
is_add_monoid_hom (λ (g : Π₀ (i : ι), β i), ⇑g i)
source
@[protected, instance]
def dfinsupp.has_neg {ι : Type u} {β : ι → Type v} [Π (i : ι), add_group (β i)] :
has_neg (Π₀ (i : ι), β i)
Equations
source
@[protected, instance]
def dfinsupp.add_comm_monoid {ι : Type u} {β : ι → Type v} [Π (i : ι), add_comm_monoid (β i)] :
add_comm_monoid (Π₀ (i : ι), β i)
Equations
source
@[simp]
theorem dfinsupp.coe_finset_sum {ι : Type u} {β : ι → Type v} {α : Type u_1} [Π (i : ι), add_comm_monoid (β i)] (s : finset α) (g : α → (Π₀ (i : ι), β i)) :
⇑∑ (a : α) in s, g a = ∑ (a : α) in s, ⇑(g a)
source
@[simp]
theorem dfinsupp.finset_sum_apply {ι : Type u} {β : ι → Type v} {α : Type u_1} [Π (i : ι), add_comm_monoid (β i)] (s : finset α) (g : α → (Π₀ (i : ι), β i)) (i : ι) :
(⇑∑ (a : α) in s, g a) i = ∑ (a : α) in s, ⇑(g a) i
source
theorem dfinsupp.neg_apply {ι : Type u} {β : ι → Type v} [Π (i : ι), add_group (β i)] (g : Π₀ (i : ι), β i) (i : ι) :
(⇑-g) i = -⇑g i
source
@[simp]
theorem dfinsupp.coe_neg {ι : Type u} {β : ι → Type v} [Π (i : ι), add_group (β i)] (g : Π₀ (i : ι), β i) :
⇑-g = -⇑g
source
@[protected, instance]
def dfinsupp.add_group {ι : Type u} {β : ι → Type v} [Π (i : ι), add_group (β i)] :
add_group (Π₀ (i : ι), β i)
Equations
source
theorem dfinsupp.sub_apply {ι : Type u} {β : ι → Type v} [Π (i : ι), add_group (β i)] (g₁ g₂ : Π₀ (i : ι), β i) (i : ι) :
⇑(g₁ - g₂) i = ⇑g₁ i - ⇑g₂ i
source
@[simp]
theorem dfinsupp.coe_sub {ι : Type u} {β : ι → Type v} [Π (i : ι), add_group (β i)] (g₁ g₂ : Π₀ (i : ι), β i) :
⇑(g₁ - g₂) = ⇑g₁ - ⇑g₂
source
@[protected, instance]
def dfinsupp.add_comm_group {ι : Type u} {β : ι → Type v} [Π (i : ι), add_comm_group (β i)] :
add_comm_group (Π₀ (i : ι), β i)
Equations
source
@[protected, instance]
def dfinsupp.has_scalar {ι : Type u} {β : ι → Type v} {γ : Type w} [monoid γ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), distrib_mul_action γ (β i)] :
has_scalar γ (Π₀ (i : ι), β i)

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

Equations
source
theorem dfinsupp.smul_apply {ι : Type u} {β : ι → Type v} {γ : Type w} [monoid γ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), distrib_mul_action γ (β i)] (b : γ) (v : Π₀ (i : ι), β i) (i : ι) :
⇑(b • v) i = b • ⇑v i
source
@[simp]
theorem dfinsupp.coe_smul {ι : Type u} {β : ι → Type v} {γ : Type w} [monoid γ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), distrib_mul_action γ (β i)] (b : γ) (v : Π₀ (i : ι), β i) :
⇑(b • v) = b • ⇑v
source
@[protected, instance]
def dfinsupp.smul_comm_class {ι : Type u} {β : ι → Type v} {γ : Type w} {δ : Type u_1} [monoid γ] [monoid δ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), distrib_mul_action γ (β i)] [Π (i : ι), distrib_mul_action δ (β i)] [∀ (i : ι), smul_comm_class γ δ (β i)] :
smul_comm_class γ δ (Π₀ (i : ι), β i)
source
@[protected, instance]
def dfinsupp.is_scalar_tower {ι : Type u} {β : ι → Type v} {γ : Type w} {δ : Type u_1} [monoid γ] [monoid δ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), distrib_mul_action γ (β i)] [Π (i : ι), distrib_mul_action δ (β i)] [has_scalar γ δ] [∀ (i : ι), is_scalar_tower γ δ (β i)] :
is_scalar_tower γ δ (Π₀ (i : ι), β i)
source
@[protected, instance]
def dfinsupp.distrib_mul_action {ι : Type u} {β : ι → Type v} {γ : Type w} [monoid γ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), distrib_mul_action γ (β i)] :
distrib_mul_action γ (Π₀ (i : ι), β i)

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

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

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

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

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

Equations
source
@[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
source
theorem dfinsupp.filter_apply_pos {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] {p : ι → Prop} [decidable_pred p] (f : Π₀ (i : ι), β i) {i : ι} (h : p i) :
⇑(dfinsupp.filter p f) i = ⇑f i
source
theorem dfinsupp.filter_apply_neg {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] {p : ι → Prop} [decidable_pred p] (f : Π₀ (i : ι), β i) {i : ι} (h : ¬p i) :
⇑(dfinsupp.filter p f) i = 0
source
theorem dfinsupp.filter_pos_add_filter_neg {ι : Type u} {β : ι → Type v} [Π (i : ι), add_zero_class (β i)] (f : Π₀ (i : ι), β i) (p : ι → Prop) [decidable_pred p] :
dfinsupp.filter p f + dfinsupp.filter (λ (i : ι), ¬p i) f = f
source
def dfinsupp.subtype_domain {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] (p : ι → Prop) [decidable_pred p] (f : Π₀ (i : ι), β i) :
Π₀ (i : subtype p), β ↑i

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

Equations
source
@[simp]
theorem dfinsupp.subtype_domain_zero {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] {p : ι → Prop} [decidable_pred p] :
dfinsupp.subtype_domain p 0 = 0
source
@[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} :
⇑(dfinsupp.subtype_domain p v) i = ⇑v ↑i
source
@[simp]
theorem dfinsupp.subtype_domain_add {ι : Type u} {β : ι → Type v} [Π (i : ι), add_zero_class (β i)] {p : ι → Prop} [decidable_pred p] {v v' : Π₀ (i : ι), β i} :
dfinsupp.subtype_domain p (v + v') = dfinsupp.subtype_domain p v + dfinsupp.subtype_domain p v'
source
@[protected, instance]
def dfinsupp.subtype_domain.is_add_monoid_hom {ι : Type u} {β : ι → Type v} [Π (i : ι), add_zero_class (β i)] {p : ι → Prop} [decidable_pred p] :
is_add_monoid_hom (dfinsupp.subtype_domain p)
source
@[simp]
theorem dfinsupp.subtype_domain_neg {ι : Type u} {β : ι → Type v} [Π (i : ι), add_group (β i)] {p : ι → Prop} [decidable_pred p] {v : Π₀ (i : ι), β i} :
dfinsupp.subtype_domain p (-v) = -dfinsupp.subtype_domain p v
source
@[simp]
theorem dfinsupp.subtype_domain_sub {ι : Type u} {β : ι → Type v} [Π (i : ι), add_group (β i)] {p : ι → Prop} [decidable_pred p] {v v' : Π₀ (i : ι), β i} :
dfinsupp.subtype_domain p (v - v') = dfinsupp.subtype_domain p v - dfinsupp.subtype_domain p v'
source
theorem dfinsupp.finite_support {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] (f : Π₀ (i : ι), β i) :
{i : ι | ⇑f i ≠ 0}.finite
source
def dfinsupp.mk {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] (s : finset ι) (x : Π (i : ↥↑s), β ↑i) :
Π₀ (i : ι), β i

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

Equations
source
@[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)
source
theorem dfinsupp.mk_injective {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] (s : finset ι) :
function.injective (dfinsupp.mk s)
source
def dfinsupp.single {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] (i : ι) (b : β i) :
Π₀ (i : ι), β i

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

Equations
source
@[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)
source
@[simp]
theorem dfinsupp.single_zero {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i : ι} :
dfinsupp.single i 0 = 0
source
@[simp]
theorem dfinsupp.single_eq_same {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i : ι} {b : β i} :
⇑(dfinsupp.single i b) i = b
source
theorem dfinsupp.single_eq_of_ne {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i i' : ι} {b : β i} (h : i ≠ i') :
⇑(dfinsupp.single i b) i' = 0
source
theorem dfinsupp.single_injective {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i : ι} :
function.injective (dfinsupp.single i)
source
theorem dfinsupp.single_eq_single_iff {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] (i j : ι) (xi : β i) (xj : β j) :
dfinsupp.single i xi = dfinsupp.single j xj ↔ i = j ∧ xi == xj ∨ xi = 0 ∧ xj = 0

Like finsupp.single_eq_single_iff, but with a heq due to dependent types

source
theorem dfinsupp.single_eq_of_sigma_eq {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i j : ι} {xi : β i} {xj : β j} (h : ⟨i, xi⟩ = ⟨j, xj⟩) :
dfinsupp.single i xi = dfinsupp.single j xj

Equality of sigma types is sufficient (but not necessary) to show equality of dfinsupps.

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

Redefine f i to be 0.

Equations
source
@[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)
source
@[simp]
theorem dfinsupp.erase_same {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i : ι} {f : Π₀ (i : ι), β i} :
⇑(dfinsupp.erase i f) i = 0
source
theorem dfinsupp.erase_ne {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i i' : ι} {f : Π₀ (i : ι), β i} (h : i' ≠ i) :
⇑(dfinsupp.erase i f) i' = ⇑f i'
source
@[simp]
theorem dfinsupp.single_add {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] {i : ι} {b₁ b₂ : β i} :
dfinsupp.single i (b₁ + b₂) = dfinsupp.single i b₁ + dfinsupp.single i b₂
source
@[simp]
theorem dfinsupp.single_add_hom_apply {ι : Type u} (β : ι → Type v) [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] (i : ι) (b : β i) :
⇑(dfinsupp.single_add_hom β i) b = dfinsupp.single i b
source
def dfinsupp.single_add_hom {ι : Type u} (β : ι → Type v) [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] (i : ι) :
β i →+ Π₀ (i : ι), β i

dfinsupp.single as an add_monoid_hom.

Equations
source
theorem dfinsupp.single_add_erase {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] {i : ι} {f : Π₀ (i : ι), β i} :
dfinsupp.single i (⇑f i) + dfinsupp.erase i f = f
source
theorem dfinsupp.erase_add_single {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] {i : ι} {f : Π₀ (i : ι), β i} :
dfinsupp.erase i f + dfinsupp.single i (⇑f i) = f
source
@[protected]
theorem dfinsupp.induction {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] {p : (Π₀ (i : ι), β i) → Prop} (f : Π₀ (i : ι), β i) (h0 : p 0) (ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), ⇑f i = 0 → b ≠ 0 → p f → p (dfinsupp.single i b + f)) :
p f
source
theorem dfinsupp.induction₂ {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] {p : (Π₀ (i : ι), β i) → Prop} (f : Π₀ (i : ι), β i) (h0 : p 0) (ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), ⇑f i = 0 → b ≠ 0 → p f → p (f + dfinsupp.single i b)) :
p f
source
@[simp]
theorem dfinsupp.add_closure_Union_range_single {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] :
add_submonoid.closure (⋃ (i : ι), set.range (dfinsupp.single i)) = ⊤
source
theorem dfinsupp.add_hom_ext {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] {γ : Type w} [add_zero_class γ] ⦃f g : (Π₀ (i : ι), β i) →+ γ⦄ (H : ∀ (i : ι) (y : β i), ⇑f (dfinsupp.single i y) = ⇑g (dfinsupp.single i y)) :
f = g

If two additive homomorphisms from Π₀ i, β i are equal on each single a b, then they are equal.

source
@[ext]
theorem dfinsupp.add_hom_ext' {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] {γ : Type w} [add_zero_class γ] ⦃f g : (Π₀ (i : ι), β i) →+ γ⦄ (H : ∀ (x : ι), f.comp (dfinsupp.single_add_hom β x) = g.comp (dfinsupp.single_add_hom β x)) :
f = g

If two additive homomorphisms from Π₀ i, β i are equal on each single a b, then they are equal.

See note [partially-applied ext lemmas].

source
@[simp]
theorem dfinsupp.mk_add {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] {s : finset ι} {x y : Π (i : ↥↑s), β ↑i} :
dfinsupp.mk s (x + y) = dfinsupp.mk s x + dfinsupp.mk s y
source
@[simp]
theorem dfinsupp.mk_zero {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {s : finset ι} :
dfinsupp.mk s 0 = 0
source
@[simp]
theorem dfinsupp.mk_neg {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_group (β i)] {s : finset ι} {x : Π (i : ↥↑s), β i.val} :
dfinsupp.mk s (-x) = -dfinsupp.mk s x
source
@[simp]
theorem dfinsupp.mk_sub {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_group (β i)] {s : finset ι} {x y : Π (i : ↥↑s), β i.val} :
dfinsupp.mk s (x - y) = dfinsupp.mk s x - dfinsupp.mk s y
source
@[protected, instance]
def dfinsupp.mk.is_add_group_hom {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_group (β i)] {s : finset ι} :
is_add_group_hom (dfinsupp.mk s)
source
@[simp]
theorem dfinsupp.mk_smul {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] (γ : Type w) [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), module γ (β i)] {s : finset ι} {c : γ} (x : Π (i : ↥↑s), β i.val) :
dfinsupp.mk s (c • x) = c • dfinsupp.mk s x
source
@[simp]
theorem dfinsupp.single_smul {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] (γ : Type w) [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), module γ (β i)] {i : ι} {c : γ} {x : β i} :
dfinsupp.single i (c • x) = c • dfinsupp.single i x
source
def dfinsupp.support {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] (f : Π₀ (i : ι), β i) :
finset ι

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

Equations
source
@[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} :
(dfinsupp.mk s x).support ⊆ s
source
@[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
source
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)
source
@[simp]
theorem dfinsupp.support_zero {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] :
0.support = ∅
source
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
source
@[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
source
@[protected, instance]
def dfinsupp.decidable_zero {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] :
decidable_pred (eq 0)
Equations
source
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 ∉ s → ⇑f i = 0
source
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} (hb : b ≠ 0) :
(dfinsupp.single i b).support = {i}
source
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} :
(dfinsupp.single i b).support ⊆ {i}
source
theorem dfinsupp.map_range_def {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [dec : decidable_eq ι] [Π (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))
source
@[simp]
theorem dfinsupp.map_range_single {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [dec : decidable_eq ι] [Π (i : ι), has_zero (β₁ i)] [Π (i : ι), has_zero (β₂ i)] {f : Π (i : ι), β₁ i → β₂ i} {hf : ∀ (i : ι), f i 0 = 0} {i : ι} {b : β₁ i} :
dfinsupp.map_range f hf (dfinsupp.single i b) = dfinsupp.single i (f i b)
source
theorem dfinsupp.support_map_range {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [dec : decidable_eq ι] [Π (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} :
(dfinsupp.map_range f hf g).support ⊆ g.support
source
theorem dfinsupp.zip_with_def {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] [Π (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))
source
theorem dfinsupp.support_zip_with {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] [Π (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
source
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) :
dfinsupp.erase i f = dfinsupp.mk (f.support.erase i) (λ (j : ↥↑(f.support.erase i)), ⇑f j.val)
source
@[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) :
(dfinsupp.erase i f).support = f.support.erase i
source
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) :
dfinsupp.filter p f = dfinsupp.mk (finset.filter p f.support) (λ (i : ↥↑(finset.filter p f.support)), ⇑f i.val)
source
@[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) :
(dfinsupp.filter p f).support = finset.filter p f.support
source
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) :
dfinsupp.subtype_domain p f = dfinsupp.mk (finset.subtype p f.support) (λ (i : ↥↑(finset.subtype p f.support)), ⇑f ↑i)
source
@[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} :
(dfinsupp.subtype_domain p f).support = finset.subtype p f.support
source
theorem dfinsupp.support_add {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] {g₁ g₂ : Π₀ (i : ι), β i} :
(g₁ + g₂).support ⊆ g₁.support ∪ g₂.support
source
@[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} :
(-f).support = f.support
source
theorem dfinsupp.support_smul {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), module γ (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] (b : γ) (v : Π₀ (i : ι), β i) :
(b • v).support ⊆ v.support
source
@[protected, 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
source
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 γ] (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i → γ) :
γ

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

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

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

Equations
source
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 → γ} (h0 : ∀ (i : ι), h i 0 = 0) :
(dfinsupp.map_range f hf g).sum h = g.sum (λ (i : ι) (b : β₁ i), h i (f i b))
source
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 → γ} (h0 : ∀ (i : ι), h i 0 = 1) :
(dfinsupp.map_range f hf g).prod h = g.prod (λ (i : ι) (b : β₁ i), h i (f i b))
source
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
source
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
source
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_zero : h i 0 = 1) :
(dfinsupp.single i b).prod h = h i b
source
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_zero : h i 0 = 0) :
(dfinsupp.single i b).sum h = h i b
source
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 → γ} (h0 : ∀ (i : ι), h i 0 = 1) :
(-g).prod h = g.prod (λ (i : ι) (b : β i), h i (-b))
source
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 → γ} (h0 : ∀ (i : ι), h i 0 = 0) :
(-g).sum h = g.sum (λ (i : ι) (b : β i), h i (-b))
source
theorem dfinsupp.sum_comm {γ : Type w} {ι₁ : Type u_1} {ι₂ : Type u_2} {β₁ : ι₁ → Type u_3} {β₂ : ι₂ → Type u_4} [decidable_eq ι₁] [decidable_eq ι₂] [Π (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) (f₂ : Π₀ (i : ι₂), β₂ i) (h : Π (i : ι₁), β₁ i → Π (i : ι₂), β₂ i → γ) :
f₁.sum (λ (i₁ : ι₁) (x₁ : β₁ i₁), f₂.sum (λ (i₂ : ι₂) (x₂ : β₂ i₂), h i₁ x₁ i₂ x₂)) = f₂.sum (λ (i₂ : ι₂) (x₂ : β₂ i₂), f₁.sum (λ (i₁ : ι₁) (x₁ : β₁ i₁), h i₁ x₁ i₂ x₂))
source
theorem dfinsupp.prod_comm {γ : Type w} {ι₁ : Type u_1} {ι₂ : Type u_2} {β₁ : ι₁ → Type u_3} {β₂ : ι₂ → Type u_4} [decidable_eq ι₁] [decidable_eq ι₂] [Π (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) (f₂ : Π₀ (i : ι₂), β₂ i) (h : Π (i : ι₁), β₁ i → Π (i : ι₂), β₂ i → γ) :
f₁.prod (λ (i₁ : ι₁) (x₁ : β₁ i₁), f₂.prod (λ (i₂ : ι₂) (x₂ : β₂ i₂), h i₁ x₁ i₂ x₂)) = f₂.prod (λ (i₂ : ι₂) (x₂ : β₂ i₂), f₁.prod (λ (i₁ : ι₁) (x₁ : β₁ i₁), h i₁ x₁ i₂ x₂))
source
@[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₂)
source
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.bUnion (λ (i : ι₁), (g i (⇑f i)).support)
source
@[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
source
@[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
source
@[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₂
source
@[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₂
source
@[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
source
@[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)⁻¹
source
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 → γ} (h_zero : ∀ (i : ι), h i 0 = 0) (h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ + h i b₂) :
(f + g).sum h = f.sum h + g.sum h
source
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 → γ} (h_zero : ∀ (i : ι), h i 0 = 1) (h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = (h i b₁) * h i b₂) :
(f + g).prod h = (f.prod h) * g.prod h
source
def dfinsupp.sum_add_hom {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_zero_class (β i)] [add_comm_monoid γ] (φ : Π (i : ι), β i →+ γ) :
(Π₀ (i : ι), β i) →+ γ

When summing over an add_monoid_hom, the decidability assumption is not needed, and the result is also an add_monoid_hom.

Equations
source
@[simp]
theorem dfinsupp.sum_add_hom_single {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_zero_class (β i)] [add_comm_monoid γ] (φ : Π (i : ι), β i →+ γ) (i : ι) (x : β i) :
⇑(dfinsupp.sum_add_hom φ) (dfinsupp.single i x) = ⇑(φ i) x
source
@[simp]
theorem dfinsupp.sum_add_hom_comp_single {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_zero_class (β i)] [add_comm_monoid γ] (f : Π (i : ι), β i →+ γ) (i : ι) :
(dfinsupp.sum_add_hom f).comp (dfinsupp.single_add_hom β i) = f i
source
theorem dfinsupp.sum_add_hom_apply {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_zero_class (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] [add_comm_monoid γ] (φ : Π (i : ι), β i →+ γ) (f : Π₀ (i : ι), β i) :
⇑(dfinsupp.sum_add_hom φ) f = f.sum (λ (x : ι), ⇑(φ x))

While we didn't need decidable instances to define it, we do to reduce it to a sum

source
theorem dfinsupp.sum_add_hom_comm {ι₁ : Type u_1} {ι₂ : Type u_2} {β₁ : ι₁ → Type u_3} {β₂ : ι₂ → Type u_4} {γ : Type u_5} [decidable_eq ι₁] [decidable_eq ι₂] [Π (i : ι₁), add_zero_class (β₁ i)] [Π (i : ι₂), add_zero_class (β₂ i)] [add_comm_monoid γ] (f₁ : Π₀ (i : ι₁), β₁ i) (f₂ : Π₀ (i : ι₂), β₂ i) (h : Π (i : ι₁) (j : ι₂), β₁ i →+ β₂ j →+ γ) :
⇑(dfinsupp.sum_add_hom (λ (i₂ : ι₂), ⇑(dfinsupp.sum_add_hom (λ (i₁ : ι₁), h i₁ i₂)) f₁)) f₂ = ⇑(dfinsupp.sum_add_hom (λ (i₁ : ι₁), ⇑(dfinsupp.sum_add_hom (λ (i₂ : ι₂), (h i₁ i₂).flip)) f₂)) f₁
source
@[simp]
theorem dfinsupp.lift_add_hom_apply {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_zero_class (β i)] [add_comm_monoid γ] (φ : Π (i : ι), (λ (i : ι), β i) i →+ γ) :
⇑dfinsupp.lift_add_hom φ = dfinsupp.sum_add_hom φ
source
@[simp]
theorem dfinsupp.lift_add_hom_symm_apply {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_zero_class (β i)] [add_comm_monoid γ] (F : (Π₀ (i : ι), β i) →+ γ) (i : ι) :
⇑(dfinsupp.lift_add_hom.symm) F i = F.comp (dfinsupp.single_add_hom β i)
source
def dfinsupp.lift_add_hom {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_zero_class (β i)] [add_comm_monoid γ] :
(Π (i : ι), β i →+ γ) ≃+ ((Π₀ (i : ι), β i) →+ γ)

The dfinsupp version of finsupp.lift_add_hom,

Equations
source
@[simp]
theorem dfinsupp.lift_add_hom_single_add_hom {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_comm_monoid (β i)] :
⇑dfinsupp.lift_add_hom (dfinsupp.single_add_hom β) = add_monoid_hom.id (Π₀ (i : ι), β i)

The dfinsupp version of finsupp.lift_add_hom_single_add_hom,

source
theorem dfinsupp.lift_add_hom_apply_single {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_zero_class (β i)] [add_comm_monoid γ] (f : Π (i : ι), β i →+ γ) (i : ι) (x : β i) :
⇑(⇑dfinsupp.lift_add_hom f) (dfinsupp.single i x) = ⇑(f i) x

The dfinsupp version of finsupp.lift_add_hom_apply_single,

source
theorem dfinsupp.lift_add_hom_comp_single {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_zero_class (β i)] [add_comm_monoid γ] (f : Π (i : ι), β i →+ γ) (i : ι) :
(⇑dfinsupp.lift_add_hom f).comp (dfinsupp.single_add_hom β i) = f i

The dfinsupp version of finsupp.lift_add_hom_comp_single,

source
theorem dfinsupp.comp_lift_add_hom {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} {δ : Type u_1} [Π (i : ι), add_zero_class (β i)] [add_comm_monoid γ] [add_comm_monoid δ] (g : γ →+ δ) (f : Π (i : ι), β i →+ γ) :
g.comp (⇑dfinsupp.lift_add_hom f) = ⇑dfinsupp.lift_add_hom (λ (a : ι), g.comp (f a))

The dfinsupp version of finsupp.comp_lift_add_hom,

source
@[simp]
theorem dfinsupp.sum_add_hom_zero {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_zero_class (β i)] [add_comm_monoid γ] :
dfinsupp.sum_add_hom (λ (i : ι), 0) = 0
source
@[simp]
theorem dfinsupp.sum_add_hom_add {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_zero_class (β i)] [add_comm_monoid γ] (g h : Π (i : ι), β i →+ γ) :
dfinsupp.sum_add_hom (λ (i : ι), g i + h i) = dfinsupp.sum_add_hom g + dfinsupp.sum_add_hom h
source
@[simp]
theorem dfinsupp.sum_add_hom_single_add_hom {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_comm_monoid (β i)] :
dfinsupp.sum_add_hom (dfinsupp.single_add_hom β) = add_monoid_hom.id (Π₀ (i : ι), β i)
source
theorem dfinsupp.comp_sum_add_hom {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} {δ : Type u_1} [Π (i : ι), add_zero_class (β i)] [add_comm_monoid γ] [add_comm_monoid δ] (g : γ →+ δ) (f : Π (i : ι), β i →+ γ) :
g.comp (dfinsupp.sum_add_hom f) = dfinsupp.sum_add_hom (λ (a : ι), g.comp (f a))
source
theorem dfinsupp.sum_sub_index {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {γ : Type w} [Π (i : ι), add_group (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] [add_comm_group γ] {f g : Π₀ (i : ι), β i} {h : Π (i : ι), β i → γ} (h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂) :
(f - g).sum h = f.sum h - g.sum h
source
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 → γ} (h_zero : ∀ (i : ι), h i 0 = 1) (h_add : ∀ (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
source
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 → γ} (h_zero : ∀ (i : ι), h i 0 = 0) (h_add : ∀ (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
source
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 → γ} (h_zero : ∀ (i : ι), h i 0 = 0) (h_add : ∀ (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)
source
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 → γ} (h_zero : ∀ (i : ι), h i 0 = 1) (h_add : ∀ (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)
source
@[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} :
f.sum dfinsupp.single = f
source
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 → γ} (hp : ∀ (x : ι), x ∈ v.support → p x) :
(dfinsupp.subtype_domain p v).sum (λ (i : subtype p) (b : β ↑i), h ↑i b) = v.sum h
source
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 → γ} (hp : ∀ (x : ι), x ∈ v.support → p x) :
(dfinsupp.subtype_domain p v).prod (λ (i : subtype p) (b : β ↑i), h ↑i b) = v.prod h
source
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)
source
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))

Bundled versions of dfinsupp.map_range #

The names should match the equivalent bundled finsupp.map_range definitions.

source
theorem dfinsupp.map_range_add {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), add_zero_class (β₁ i)] [Π (i : ι), add_zero_class (β₂ i)] (f : Π (i : ι), β₁ i → β₂ i) (hf : ∀ (i : ι), f i 0 = 0) (hf' : ∀ (i : ι) (x y : β₁ i), f i (x + y) = f i x + f i y) (g₁ g₂ : Π₀ (i : ι), β₁ i) :
dfinsupp.map_range f hf (g₁ + g₂) = dfinsupp.map_range f hf g₁ + dfinsupp.map_range f hf g₂
source
@[simp]
theorem dfinsupp.map_range.add_monoid_hom_apply {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), add_zero_class (β₁ i)] [Π (i : ι), add_zero_class (β₂ i)] (f : Π (i : ι), β₁ i →+ β₂ i) (g : Π₀ (i : ι), (λ (i : ι), β₁ i) i) :
⇑(dfinsupp.map_range.add_monoid_hom f) g = dfinsupp.map_range (λ (i : ι) (x : β₁ i), ⇑(f i) x) _ g
source
def dfinsupp.map_range.add_monoid_hom {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), add_zero_class (β₁ i)] [Π (i : ι), add_zero_class (β₂ i)] (f : Π (i : ι), β₁ i →+ β₂ i) :
(Π₀ (i : ι), β₁ i) →+ Π₀ (i : ι), β₂ i

dfinsupp.map_range as an add_monoid_hom.

Equations
source
@[simp]
theorem dfinsupp.map_range.add_monoid_hom_id {ι : Type u} {β₂ : ι → Type v₂} [Π (i : ι), add_zero_class (β₂ i)] :
dfinsupp.map_range.add_monoid_hom (λ (i : ι), add_monoid_hom.id (β₂ i)) = add_monoid_hom.id (Π₀ (i : ι), β₂ i)
source
theorem dfinsupp.map_range.add_monoid_hom_comp {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), add_zero_class (β i)] [Π (i : ι), add_zero_class (β₁ i)] [Π (i : ι), add_zero_class (β₂ i)] (f : Π (i : ι), β₁ i →+ β₂ i) (f₂ : Π (i : ι), β i →+ β₁ i) :
dfinsupp.map_range.add_monoid_hom (λ (i : ι), (f i).comp (f₂ i)) = (dfinsupp.map_range.add_monoid_hom f).comp (dfinsupp.map_range.add_monoid_hom f₂)
source
def dfinsupp.map_range.add_equiv {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), add_zero_class (β₁ i)] [Π (i : ι), add_zero_class (β₂ i)] (e : Π (i : ι), β₁ i ≃+ β₂ i) :
(Π₀ (i : ι), β₁ i) ≃+ Π₀ (i : ι), β₂ i

dfinsupp.map_range.add_monoid_hom as an add_equiv.

Equations
source
@[simp]
theorem dfinsupp.map_range.add_equiv_apply {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), add_zero_class (β₁ i)] [Π (i : ι), add_zero_class (β₂ i)] (e : Π (i : ι), β₁ i ≃+ β₂ i) (g : Π₀ (i : ι), (λ (i : ι), β₁ i) i) :
⇑(dfinsupp.map_range.add_equiv e) g = dfinsupp.map_range (λ (i : ι) (x : β₁ i), ⇑(e i) x) _ g
source
@[simp]
theorem dfinsupp.map_range.add_equiv_refl {ι : Type u} {β₁ : ι → Type v₁} [Π (i : ι), add_zero_class (β₁ i)] :
dfinsupp.map_range.add_equiv (λ (i : ι), add_equiv.refl (β₁ i)) = add_equiv.refl (Π₀ (i : ι), β₁ i)
source
theorem dfinsupp.map_range.add_equiv_trans {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), add_zero_class (β i)] [Π (i : ι), add_zero_class (β₁ i)] [Π (i : ι), add_zero_class (β₂ i)] (f : Π (i : ι), β i ≃+ β₁ i) (f₂ : Π (i : ι), β₁ i ≃+ β₂ i) :
dfinsupp.map_range.add_equiv (λ (i : ι), (f i).trans (f₂ i)) = (dfinsupp.map_range.add_equiv f).trans (dfinsupp.map_range.add_equiv f₂)
source
@[simp]
theorem dfinsupp.map_range.add_equiv_symm {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [Π (i : ι), add_zero_class (β₁ i)] [Π (i : ι), add_zero_class (β₂ i)] (e : Π (i : ι), β₁ i ≃+ β₂ i) :
(dfinsupp.map_range.add_equiv e).symm = dfinsupp.map_range.add_equiv (λ (i : ι), (e i).symm)

Product and sum lemmas for bundled morphisms #

source
@[simp]
theorem add_monoid_hom.map_dfinsupp_sum {ι : Type u} {β : ι → Type v} [decidable_eq ι] {R : Type u_1} {S : Type u_2} [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] [add_comm_monoid R] [add_comm_monoid S] (h : R →+ S) (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i → R) :
⇑h (f.sum g) = f.sum (λ (a : ι) (b : β a), ⇑h (g a b))
source
@[simp]
theorem monoid_hom.map_dfinsupp_prod {ι : Type u} {β : ι → Type v} [decidable_eq ι] {R : Type u_1} {S : Type u_2} [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] [comm_monoid R] [comm_monoid S] (h : R →* S) (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i → R) :
⇑h (f.prod g) = f.prod (λ (a : ι) (b : β a), ⇑h (g a b))
source
theorem add_monoid_hom.coe_dfinsupp_sum {ι : Type u} {β : ι → Type v} [decidable_eq ι] {R : Type u_1} {S : Type u_2} [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] [add_monoid R] [add_comm_monoid S] (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i → R →+ S) :
⇑(f.sum g) = f.sum (λ (a : ι) (b : β a), ⇑(g a b))
source
theorem monoid_hom.coe_dfinsupp_prod {ι : Type u} {β : ι → Type v} [decidable_eq ι] {R : Type u_1} {S : Type u_2} [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] [monoid R] [comm_monoid S] (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i → R →* S) :
⇑(f.prod g) = f.prod (λ (a : ι) (b : β a), ⇑(g a b))
source
@[simp]
theorem monoid_hom.dfinsupp_prod_apply {ι : Type u} {β : ι → Type v} [decidable_eq ι] {R : Type u_1} {S : Type u_2} [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] [monoid R] [comm_monoid S] (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i → R →* S) (r : R) :
⇑(f.prod g) r = f.prod (λ (a : ι) (b : β a), ⇑(g a b) r)
source
@[simp]
theorem add_monoid_hom.dfinsupp_sum_apply {ι : Type u} {β : ι → Type v} [decidable_eq ι] {R : Type u_1} {S : Type u_2} [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] [add_monoid R] [add_comm_monoid S] (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i → R →+ S) (r : R) :
⇑(f.sum g) r = f.sum (λ (a : ι) (b : β a), ⇑(g a b) r)

The above lemmas, repeated for dfinsupp.sum_add_hom.

source
@[simp]
theorem add_monoid_hom.map_dfinsupp_sum_add_hom {ι : Type u} {β : ι → Type v} [decidable_eq ι] {R : Type u_1} {S : Type u_2} [add_comm_monoid R] [add_comm_monoid S] [Π (i : ι), add_comm_monoid (β i)] (h : R →+ S) (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i →+ R) :
⇑h (⇑(dfinsupp.sum_add_hom g) f) = ⇑(dfinsupp.sum_add_hom (λ (i : ι), h.comp (g i))) f
source
@[simp]
theorem add_monoid_hom.dfinsupp_sum_add_hom_apply {ι : Type u} {β : ι → Type v} [decidable_eq ι] {R : Type u_1} {S : Type u_2} [add_zero_class R] [add_comm_monoid S] [Π (i : ι), add_comm_monoid (β i)] (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i →+ R →+ S) (r : R) :
⇑(⇑(dfinsupp.sum_add_hom g) f) r = ⇑(dfinsupp.sum_add_hom (λ (i : ι), (⇑add_monoid_hom.eval r).comp (g i))) f
source
theorem add_monoid_hom.coe_dfinsupp_sum_add_hom {ι : Type u} {β : ι → Type v} [decidable_eq ι] {R : Type u_1} {S : Type u_2} [add_zero_class R] [add_comm_monoid S] [Π (i : ι), add_comm_monoid (β i)] (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i →+ R →+ S) :
⇑(⇑(dfinsupp.sum_add_hom g) f) = ⇑(dfinsupp.sum_add_hom (λ (i : ι), (add_monoid_hom.coe_fn R S).comp (g i))) f