data.dfinsupp.basic - mathlib3 docs

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

Type (max u v)

to_fun : Π (i : ι), β i
support' : trunc {s // ∀ (i : ι), i ∈ s ∨ self.to_fun i = 0}

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

Note that dfinsupp.support is the preferred API for accessing the support of the function, dfinsupp.support' is a implementation detail that aids computability; see the implementation notes in this file for more information.

Instances for dfinsupp

source

@[protected, instance]

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

fun_like (Π₀ (i : ι), β i) ι β

Equations

dfinsupp.fun_like = {coe := λ (f : Π₀ (i : ι), β i), f.to_fun, coe_injective' := _}

source

@[protected, instance]

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

has_coe_to_fun (Π₀ (i : ι), β i) (λ (_x : Π₀ (i : ι), β i), Π (i : ι), β i)

Helper instance for when there are too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations

dfinsupp.has_coe_to_fun = fun_like.has_coe_to_fun

source

@[simp]

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

f.to_fun = ⇑f

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

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

f = g ↔ ∀ (i : ι), ⇑f i = ⇑g i

Deprecated. Use fun_like.ext_iff instead.

source

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

function.injective coe_fn

Deprecated. Use fun_like.coe_injective instead.

source

@[protected, instance]

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

has_zero (Π₀ (i : ι), β i)

Equations

dfinsupp.has_zero = {zero := {to_fun := 0, support' := trunc.mk ⟨∅, _⟩}}

source

@[protected, instance]

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

inhabited (Π₀ (i : ι), β i)

Equations

dfinsupp.inhabited = {default := 0}

source

@[simp]

theorem dfinsupp.coe_mk' {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] (f : Π (i : ι), β i) (s : trunc {s // ∀ (i : ι), i ∈ s ∨ f i = 0}) :

⇑{to_fun := f, support' := s} = f

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

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) (x : Π₀ (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

dfinsupp.map_range f hf x = {to_fun := λ (i : ι), f i (⇑x i), support' := trunc.map (λ (s : {s // ∀ (i : ι), i ∈ s ∨ x.to_fun i = 0}), ⟨↑s, _⟩) x.support'}

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) (x : Π₀ (i : ι), β₁ i) (y : Π₀ (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

dfinsupp.zip_with f hf x y = {to_fun := λ (i : ι), f i (⇑x i) (⇑y i), support' := x.support'.bind (λ (xs : {s // ∀ (i : ι), i ∈ s ∨ x.to_fun i = 0}), trunc.map (λ (ys : {s // ∀ (i : ι), i ∈ s ∨ y.to_fun i = 0}), ⟨↑xs + ↑ys, _⟩) y.support')}

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

def dfinsupp.piecewise {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] (x y : Π₀ (i : ι), β i) (s : set ι) [Π (i : ι), decidable (i ∈ s)] :

Π₀ (i : ι), β i

x.piecewise y s is the finitely supported function equal to x on the set s, and to y on its complement.

Equations

x.piecewise y s = dfinsupp.zip_with (λ (i : ι) (x y : β i), ite (i ∈ s) x y) _ x y

source

theorem dfinsupp.piecewise_apply {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] (x y : Π₀ (i : ι), β i) (s : set ι) [Π (i : ι), decidable (i ∈ s)] (i : ι) :

⇑(x.piecewise y s) i = ite (i ∈ s) (⇑x i) (⇑y i)

source

@[simp, norm_cast]

theorem dfinsupp.coe_piecewise {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] (x y : Π₀ (i : ι), β i) (s : set ι) [Π (i : ι), decidable (i ∈ s)] :

⇑(x.piecewise y s) = s.piecewise ⇑x ⇑y

source

@[protected, instance]

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

has_add (Π₀ (i : ι), β i)

Equations

dfinsupp.has_add = {add := dfinsupp.zip_with (λ (_x : ι), has_add.add) dfinsupp.has_add._proof_1}

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

dfinsupp.add_zero_class = function.injective.add_zero_class coe_fn dfinsupp.add_zero_class._proof_1 dfinsupp.add_zero_class._proof_2 dfinsupp.add_zero_class._proof_3

source

@[protected, instance]

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

has_smul ℕ (Π₀ (i : ι), β i)

Note the general dfinsupp.has_smul instance doesn't apply as ℕ is not distributive unless β i's addition is commutative.

Equations

dfinsupp.has_nat_scalar = {smul := λ (c : ℕ) (v : Π₀ (i : ι), β i), dfinsupp.map_range (λ (_x : ι), has_smul.smul c) _ v}

source

theorem dfinsupp.nsmul_apply {ι : Type u} {β : ι → Type v} [Π (i : ι), add_monoid (β i)] (b : ℕ) (v : Π₀ (i : ι), β i) (i : ι) :

⇑(b • v) i = b • ⇑v i

source

@[simp]

theorem dfinsupp.coe_nsmul {ι : Type u} {β : ι → Type v} [Π (i : ι), add_monoid (β i)] (b : ℕ) (v : Π₀ (i : ι), β i) :

⇑(b • v) = b • ⇑v

source

@[protected, instance]

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

add_monoid (Π₀ (i : ι), β i)

Equations

dfinsupp.add_monoid = function.injective.add_monoid coe_fn dfinsupp.add_monoid._proof_1 dfinsupp.add_monoid._proof_2 dfinsupp.add_monoid._proof_3 dfinsupp.add_monoid._proof_4

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

dfinsupp.coe_fn_add_monoid_hom = {to_fun := coe_fn dfinsupp.has_coe_to_fun, map_zero' := _, map_add' := _}

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 pi.eval_add_monoid_hom.

Equations

dfinsupp.eval_add_monoid_hom i = (pi.eval_add_monoid_hom β i).comp dfinsupp.coe_fn_add_monoid_hom

source

@[protected, instance]

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

add_comm_monoid (Π₀ (i : ι), β i)

Equations

dfinsupp.add_comm_monoid = function.injective.add_comm_monoid coe_fn dfinsupp.add_comm_monoid._proof_1 dfinsupp.add_comm_monoid._proof_2 dfinsupp.add_comm_monoid._proof_3 dfinsupp.add_comm_monoid._proof_4

source

@[simp]

theorem dfinsupp.coe_finset_sum {ι : Type u} {β : ι → Type v} {α : Type u_1} [Π (i : ι), add_comm_monoid (β i)] (s : finset α) (g : α → (Π₀ (i : ι), β i)) :

⇑(s.sum (λ (a : α), g a)) = s.sum (λ (a : α), ⇑(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 : ι) :

⇑(s.sum (λ (a : α), g a)) i = s.sum (λ (a : α), ⇑(g a) i)

source

@[protected, instance]

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

has_neg (Π₀ (i : ι), β i)

Equations

dfinsupp.has_neg = {neg := λ (f : Π₀ (i : ι), β i), dfinsupp.map_range (λ (_x : ι), has_neg.neg) dfinsupp.has_neg._proof_1 f}

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.has_sub {ι : Type u} {β : ι → Type v} [Π (i : ι), add_group (β i)] :

has_sub (Π₀ (i : ι), β i)

Equations

dfinsupp.has_sub = {sub := dfinsupp.zip_with (λ (_x : ι), has_sub.sub) dfinsupp.has_sub._proof_1}

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.has_int_scalar {ι : Type u} {β : ι → Type v} [Π (i : ι), add_group (β i)] :

has_smul ℤ (Π₀ (i : ι), β i)

Note the general dfinsupp.has_smul instance doesn't apply as ℤ is not distributive unless β i's addition is commutative.

Equations

dfinsupp.has_int_scalar = {smul := λ (c : ℤ) (v : Π₀ (i : ι), β i), dfinsupp.map_range (λ (_x : ι), has_smul.smul c) _ v}

source

theorem dfinsupp.zsmul_apply {ι : Type u} {β : ι → Type v} [Π (i : ι), add_group (β i)] (b : ℤ) (v : Π₀ (i : ι), β i) (i : ι) :

⇑(b • v) i = b • ⇑v i

source

@[simp]

theorem dfinsupp.coe_zsmul {ι : Type u} {β : ι → Type v} [Π (i : ι), add_group (β i)] (b : ℤ) (v : Π₀ (i : ι), β i) :

⇑(b • v) = b • ⇑v

source

@[protected, instance]

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

add_group (Π₀ (i : ι), β i)

Equations

dfinsupp.add_group = function.injective.add_group coe_fn dfinsupp.add_group._proof_1 dfinsupp.add_group._proof_2 dfinsupp.add_group._proof_3 dfinsupp.add_group._proof_4 dfinsupp.add_group._proof_5 dfinsupp.add_group._proof_6 dfinsupp.add_group._proof_7

source

@[protected, instance]

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

add_comm_group (Π₀ (i : ι), β i)

Equations

dfinsupp.add_comm_group = function.injective.add_comm_group coe_fn dfinsupp.add_comm_group._proof_1 dfinsupp.add_comm_group._proof_2 dfinsupp.add_comm_group._proof_3 dfinsupp.add_comm_group._proof_4 dfinsupp.add_comm_group._proof_5 dfinsupp.add_comm_group._proof_6 dfinsupp.add_comm_group._proof_7

source

@[protected, instance]

def dfinsupp.has_smul {ι : Type u} {γ : Type w} {β : ι → Type v} [monoid γ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), distrib_mul_action γ (β i)] :

has_smul γ (Π₀ (i : ι), β i)

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

Equations

dfinsupp.has_smul = {smul := λ (c : γ) (v : Π₀ (i : ι), β i), dfinsupp.map_range (λ (_x : ι), has_smul.smul c) _ v}

source

theorem dfinsupp.smul_apply {ι : Type u} {γ : Type w} {β : ι → Type v} [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 w} {β : ι → Type v} [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 w} {β : ι → Type v} {δ : 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 w} {β : ι → Type v} {δ : Type u_1} [monoid γ] [monoid δ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), distrib_mul_action γ (β i)] [Π (i : ι), distrib_mul_action δ (β i)] [has_smul γ δ] [∀ (i : ι), is_scalar_tower γ δ (β i)] :

is_scalar_tower γ δ (Π₀ (i : ι), β i)

source

@[protected, instance]

def dfinsupp.is_central_scalar {ι : Type u} {γ : Type w} {β : ι → Type v} [monoid γ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), distrib_mul_action γ (β i)] [Π (i : ι), distrib_mul_action γᵐᵒᵖ (β i)] [∀ (i : ι), is_central_scalar γ (β i)] :

is_central_scalar γ (Π₀ (i : ι), β i)

source

@[protected, instance]

def dfinsupp.distrib_mul_action {ι : Type u} {γ : Type w} {β : ι → Type v} [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

dfinsupp.distrib_mul_action = function.injective.distrib_mul_action dfinsupp.coe_fn_add_monoid_hom dfinsupp.distrib_mul_action._proof_1 dfinsupp.distrib_mul_action._proof_2

source

@[protected, instance]

def dfinsupp.module {ι : Type u} {γ : Type w} {β : ι → Type v} [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

dfinsupp.module = {to_distrib_mul_action := {to_mul_action := distrib_mul_action.to_mul_action dfinsupp.distrib_mul_action, smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}

source

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

Π₀ (i : ι), β i

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

Equations

dfinsupp.filter p x = {to_fun := λ (i : ι), ite (p i) (⇑x i) 0, support' := trunc.map (λ (xs : {s // ∀ (i : ι), i ∈ s ∨ x.to_fun i = 0}), ⟨↑xs, _⟩) x.support'}

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

@[simp]

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

dfinsupp.filter p 0 = 0

source

@[simp]

theorem dfinsupp.filter_add {ι : Type u} {β : ι → Type v} [Π (i : ι), add_zero_class (β i)] (p : ι → Prop) [decidable_pred p] (f g : Π₀ (i : ι), β i) :

dfinsupp.filter p (f + g) = dfinsupp.filter p f + dfinsupp.filter p g

source

@[simp]

theorem dfinsupp.filter_smul {ι : Type u} {γ : Type w} {β : ι → Type v} [monoid γ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), distrib_mul_action γ (β i)] (p : ι → Prop) [decidable_pred p] (r : γ) (f : Π₀ (i : ι), β i) :

dfinsupp.filter p (r • f) = r • dfinsupp.filter p f

source

def dfinsupp.filter_add_monoid_hom {ι : Type u} (β : ι → Type v) [Π (i : ι), add_zero_class (β i)] (p : ι → Prop) [decidable_pred p] :

(Π₀ (i : ι), β i) →+ Π₀ (i : ι), β i

dfinsupp.filter as an add_monoid_hom.

Equations

dfinsupp.filter_add_monoid_hom β p = {to_fun := dfinsupp.filter p (λ (a : ι), _inst_2 a), map_zero' := _, map_add' := _}

source

@[simp]

theorem dfinsupp.filter_add_monoid_hom_apply {ι : Type u} (β : ι → Type v) [Π (i : ι), add_zero_class (β i)] (p : ι → Prop) [decidable_pred p] (x : Π₀ (i : ι), (λ (i : ι), β i) i) :

⇑(dfinsupp.filter_add_monoid_hom β p) x = dfinsupp.filter p x

source

@[simp]

theorem dfinsupp.filter_linear_map_apply {ι : Type u} (γ : Type w) (β : ι → Type v) [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), module γ (β i)] (p : ι → Prop) [decidable_pred p] (x : Π₀ (i : ι), (λ (i : ι), β i) i) :

⇑(dfinsupp.filter_linear_map γ β p) x = dfinsupp.filter p x

source

def dfinsupp.filter_linear_map {ι : Type u} (γ : Type w) (β : ι → Type v) [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), module γ (β i)] (p : ι → Prop) [decidable_pred p] :

(Π₀ (i : ι), β i) →ₗ[γ] Π₀ (i : ι), β i

dfinsupp.filter as a linear_map.

Equations

dfinsupp.filter_linear_map γ β p = {to_fun := dfinsupp.filter p (λ (a : ι), _inst_4 a), map_add' := _, map_smul' := _}

source

@[simp]

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

dfinsupp.filter p (-f) = -dfinsupp.filter p f

source

@[simp]

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

dfinsupp.filter p (f - g) = dfinsupp.filter p f - dfinsupp.filter p g

source

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

Π₀ (i : subtype p), β ↑i

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

Equations

dfinsupp.subtype_domain p x = {to_fun := λ (i : subtype p), ⇑x ↑i, support' := trunc.map (λ (xs : {s // ∀ (i : ι), i ∈ s ∨ x.to_fun i = 0}), ⟨multiset.map (λ (j : {x_1 // x_1 ∈ multiset.filter p ↑xs}), ⟨↑j, _⟩) (multiset.filter p ↑xs).attach, _⟩) x.support'}

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

@[simp]

theorem dfinsupp.subtype_domain_smul {ι : Type u} {γ : Type w} {β : ι → Type v} [monoid γ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), distrib_mul_action γ (β i)] {p : ι → Prop} [decidable_pred p] (r : γ) (f : Π₀ (i : ι), β i) :

dfinsupp.subtype_domain p (r • f) = r • dfinsupp.subtype_domain p f

source

def dfinsupp.subtype_domain_add_monoid_hom {ι : Type u} (β : ι → Type v) [Π (i : ι), add_zero_class (β i)] (p : ι → Prop) [decidable_pred p] :

(Π₀ (i : ι), β i) →+ Π₀ (i : subtype p), β ↑i

subtype_domain but as an add_monoid_hom.

Equations

dfinsupp.subtype_domain_add_monoid_hom β p = {to_fun := dfinsupp.subtype_domain p (λ (a : ι), _inst_2 a), map_zero' := _, map_add' := _}

source

@[simp]

theorem dfinsupp.subtype_domain_add_monoid_hom_apply {ι : Type u} (β : ι → Type v) [Π (i : ι), add_zero_class (β i)] (p : ι → Prop) [decidable_pred p] (x : Π₀ (i : ι), (λ (i : ι), β i) i) :

⇑(dfinsupp.subtype_domain_add_monoid_hom β p) x = dfinsupp.subtype_domain p x

source

def dfinsupp.subtype_domain_linear_map {ι : Type u} (γ : Type w) (β : ι → Type v) [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), module γ (β i)] (p : ι → Prop) [decidable_pred p] :

(Π₀ (i : ι), β i) →ₗ[γ] Π₀ (i : subtype p), β ↑i

dfinsupp.subtype_domain as a linear_map.

Equations

dfinsupp.subtype_domain_linear_map γ β p = {to_fun := dfinsupp.subtype_domain p (λ (a : ι), _inst_4 a), map_add' := _, map_smul' := _}

source

@[simp]

theorem dfinsupp.subtype_domain_linear_map_apply {ι : Type u} (γ : Type w) (β : ι → Type v) [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), module γ (β i)] (p : ι → Prop) [decidable_pred p] (x : Π₀ (i : ι), (λ (i : ι), β i) i) :

⇑(dfinsupp.subtype_domain_linear_map γ β p) x = dfinsupp.subtype_domain p x

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

dfinsupp.mk s x = {to_fun := λ (i : ι), dite (i ∈ s) (λ (H : i ∈ s), x ⟨i, H⟩) (λ (H : i ∉ s), 0), support' := trunc.mk ⟨s.val, _⟩}

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_of_mem {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {s : finset ι} {x : Π (i : ↥↑s), β ↑i} {i : ι} (hi : i ∈ s) :

⇑(dfinsupp.mk s x) i = x ⟨i, hi⟩

source

theorem dfinsupp.mk_of_not_mem {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {s : finset ι} {x : Π (i : ↥↑s), β ↑i} {i : ι} (hi : i ∉ s) :

⇑(dfinsupp.mk s x) i = 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

@[protected, instance]

def dfinsupp.unique {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] [∀ (i : ι), subsingleton (β i)] :

unique (Π₀ (i : ι), β i)

Equations

dfinsupp.unique = dfinsupp.unique._proof_2.unique

source

@[protected, instance]

def dfinsupp.unique_of_is_empty {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] [is_empty ι] :

unique (Π₀ (i : ι), β i)

Equations

dfinsupp.unique_of_is_empty = dfinsupp.unique_of_is_empty._proof_2.unique

source

def dfinsupp.equiv_fun_on_fintype {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] [fintype ι] :

(Π₀ (i : ι), β i) ≃ Π (i : ι), β i

Given fintype ι, equiv_fun_on_fintype is the equiv between Π₀ i, β i and Π i, β i. (All dependent functions on a finite type are finitely supported.)

Equations

dfinsupp.equiv_fun_on_fintype = {to_fun := coe_fn dfinsupp.has_coe_to_fun, inv_fun := λ (f : Π (i : ι), β i), {to_fun := f, support' := trunc.mk ⟨finset.univ.val, _⟩}, left_inv := _, right_inv := _}

source

@[simp]

theorem dfinsupp.equiv_fun_on_fintype_apply {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] [fintype ι] (x : Π₀ (i : ι), β i) (i : ι) :

⇑dfinsupp.equiv_fun_on_fintype x i = ⇑x i

source

@[simp]

theorem dfinsupp.equiv_fun_on_fintype_symm_coe {ι : Type u} {β : ι → Type v} [Π (i : ι), has_zero (β i)] [fintype ι] (f : Π₀ (i : ι), β i) :

⇑(dfinsupp.equiv_fun_on_fintype.symm) ⇑f = f

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

dfinsupp.single i b = {to_fun := pi.single i b, support' := trunc.mk ⟨{i}, _⟩}

source

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

⇑(dfinsupp.single i b) = pi.single i b

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_left_injective {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {b : Π (i : ι), β i} (h : ∀ (i : ι), b i ≠ 0) :

function.injective (λ (i : ι), dfinsupp.single i (b i))

dfinsupp.single a b is injective in a. For the statement that it is injective in b, see dfinsupp.single_injective

source

@[simp]

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

dfinsupp.single i xi = 0 ↔ xi = 0

source

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

dfinsupp.filter p (dfinsupp.single i x) = ite (p i) (dfinsupp.single i x) 0

source

@[simp]

theorem dfinsupp.filter_single_pos {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {p : ι → Prop} [decidable_pred p] (i : ι) (x : β i) (h : p i) :

dfinsupp.filter p (dfinsupp.single i x) = dfinsupp.single i x

source

@[simp]

theorem dfinsupp.filter_single_neg {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {p : ι → Prop} [decidable_pred p] (i : ι) (x : β i) (h : ¬p i) :

dfinsupp.filter p (dfinsupp.single i x) = 0

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

@[simp]

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

⇑dfinsupp.equiv_fun_on_fintype (dfinsupp.single i m) = pi.single i m

source

@[simp]

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

⇑(dfinsupp.equiv_fun_on_fintype.symm) (pi.single i m) = dfinsupp.single i m

source

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

Π₀ (i : ι), β i

Redefine f i to be 0.

Equations

dfinsupp.erase i x = {to_fun := λ (j : ι), ite (j = i) 0 (x.to_fun j), support' := trunc.map (λ (xs : {s // ∀ (i : ι), i ∈ s ∨ x.to_fun i = 0}), ⟨↑xs, _⟩) x.support'}

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

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

(dfinsupp.single i (⇑x i)).piecewise (dfinsupp.erase i x) {i} = x

source

theorem dfinsupp.erase_eq_sub_single {ι : Type u} [dec : decidable_eq ι] {β : ι → Type u_1} [Π (i : ι), add_group (β i)] (f : Π₀ (i : ι), β i) (i : ι) :

dfinsupp.erase i f = f - dfinsupp.single i (⇑f i)

source

@[simp]

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

dfinsupp.erase i 0 = 0

source

@[simp]

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

dfinsupp.filter (λ (_x : ι), _x ≠ i) f = dfinsupp.erase i f

source

@[simp]

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

dfinsupp.filter (ne i) f = dfinsupp.erase i f

source

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

dfinsupp.erase j (dfinsupp.single i x) = ite (i = j) 0 (dfinsupp.single i x)

source

@[simp]

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

dfinsupp.erase i (dfinsupp.single i x) = 0

source

@[simp]

theorem dfinsupp.erase_single_ne {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i j : ι} (x : β i) (h : i ≠ j) :

dfinsupp.erase j (dfinsupp.single i x) = dfinsupp.single i x

source

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

Π₀ (i : ι), β i

Replace the value of a Π₀ i, β i at a given point i : ι by a given value b : β i. If b = 0, this amounts to removing i from the support. Otherwise, i is added to it.

This is the (dependent) finitely-supported version of function.update.

Equations

dfinsupp.update i f b = {to_fun := function.update ⇑f i b, support' := trunc.map (λ (s : {s // ∀ (i : ι), i ∈ s ∨ f.to_fun i = 0}), ⟨i ::ₘ ↑s, _⟩) f.support'}

source

@[simp]

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

⇑(dfinsupp.update i f b) = function.update ⇑f i b

source

@[simp]

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

dfinsupp.update i f (⇑f i) = f

source

@[simp]

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

dfinsupp.update i f 0 = dfinsupp.erase i f

source

theorem dfinsupp.update_eq_single_add_erase {ι : Type u} [dec : decidable_eq ι] {β : ι → Type u_1} [Π (i : ι), add_zero_class (β i)] (f : Π₀ (i : ι), β i) (i : ι) (b : β i) :

dfinsupp.update i f b = dfinsupp.single i b + dfinsupp.erase i f

source

theorem dfinsupp.update_eq_erase_add_single {ι : Type u} [dec : decidable_eq ι] {β : ι → Type u_1} [Π (i : ι), add_zero_class (β i)] (f : Π₀ (i : ι), β i) (i : ι) (b : β i) :

dfinsupp.update i f b = dfinsupp.erase i f + dfinsupp.single i b

source

theorem dfinsupp.update_eq_sub_add_single {ι : Type u} [dec : decidable_eq ι] {β : ι → Type u_1} [Π (i : ι), add_group (β i)] (f : Π₀ (i : ι), β i) (i : ι) (b : β i) :

dfinsupp.update i f b = f - dfinsupp.single i (⇑f i) + dfinsupp.single i b

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.erase_add {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] (i : ι) (f₁ f₂ : Π₀ (i : ι), β i) :

dfinsupp.erase i (f₁ + f₂) = dfinsupp.erase i f₁ + dfinsupp.erase i f₂

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

dfinsupp.single_add_hom β i = {to_fun := dfinsupp.single i, map_zero' := _, map_add' := _}

source

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

(Π₀ (i : ι), β i) →+ Π₀ (i : ι), β i

dfinsupp.erase as an add_monoid_hom.

Equations

dfinsupp.erase_add_hom β i = {to_fun := dfinsupp.erase i, map_zero' := _, map_add' := _}

source

@[simp]

theorem dfinsupp.erase_add_hom_apply {ι : Type u} (β : ι → Type v) [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] (i : ι) (x : Π₀ (i : ι), (λ (i : ι), β i) i) :

⇑(dfinsupp.erase_add_hom β i) x = dfinsupp.erase i x

source

@[simp]

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

dfinsupp.single i (-x) = -dfinsupp.single i x

source

@[simp]

theorem dfinsupp.single_sub {ι : Type u} [dec : decidable_eq ι] {β : ι → Type v} [Π (i : ι), add_group (β i)] (i : ι) (x y : β i) :

dfinsupp.single i (x - y) = dfinsupp.single i x - dfinsupp.single i y

source

@[simp]

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

dfinsupp.erase i (-f) = -dfinsupp.erase i f

source

@[simp]

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

dfinsupp.erase i (f - g) = dfinsupp.erase i f - dfinsupp.erase i g

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

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

(Π (i : ↥↑s), β ↑i) →+ Π₀ (i : ι), β i

If s is a subset of ι then mk_add_group_hom s is the canonical additive group homomorphism from $\prod_{i\in s}\beta_i$ to $\prod_{\mathtt{i : \iota}}\beta_i.$

Equations

dfinsupp.mk_add_group_hom s = {to_fun := dfinsupp.mk s, map_zero' := _, map_add' := _}

source

@[simp]

theorem dfinsupp.mk_smul {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : decidable_eq ι] [monoid γ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), distrib_mul_action γ (β i)] {s : finset ι} (c : γ) (x : Π (i : ↥↑s), β ↑i) :

dfinsupp.mk s (c • x) = c • dfinsupp.mk s x

source

@[simp]

theorem dfinsupp.single_smul {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : decidable_eq ι] [monoid γ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), distrib_mul_action γ (β 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

f.support = trunc.lift (λ (xs : {s // ∀ (i : ι), i ∈ s ∨ f.to_fun i = 0}), finset.filter (λ (i : ι), ⇑f i ≠ 0) ↑xs.to_finset) _ f.support'

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.support_mk'_subset {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] {f : Π (i : ι), β i} {s : multiset ι} {h : ∀ (i : ι), i ∈ s ∨ f i = 0} :

{to_fun := f, support' := trunc.mk ⟨s, h⟩}.support ⊆ s.to_finset

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

theorem dfinsupp.not_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

dfinsupp.decidable_zero = λ (f : Π₀ (i : ι), β i), decidable_of_iff (f.support = ∅) _

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 : ι), 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.support_update_ne_zero {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] (f : Π₀ (i : ι), β i) (i : ι) {b : β i} (h : b ≠ 0) :

(dfinsupp.update i f b).support = has_insert.insert i f.support

source

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

(dfinsupp.update i f b).support = ite (b = 0) (dfinsupp.erase i f).support (has_insert.insert i f.support)

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

dfinsupp.decidable_eq = λ (f g : Π₀ (i : ι), β i), decidable_of_iff (f.support = g.support ∧ ∀ (i : ι), i ∈ f.support → ⇑f i = ⇑g i) _

source

noncomputable def dfinsupp.comap_domain {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {κ : Type u_1} [Π (i : ι), has_zero (β i)] (h : κ → ι) (hh : function.injective h) (f : Π₀ (i : ι), β i) :

Π₀ (k : κ), β (h k)

Reindexing (and possibly removing) terms of a dfinsupp.

Equations

dfinsupp.comap_domain h hh f = {to_fun := λ (x : κ), ⇑f (h x), support' := trunc.map (λ (s : {s // ∀ (i : ι), i ∈ s ∨ f.to_fun i = 0}), ⟨(↑s.to_finset.preimage h _).val, _⟩) f.support'}

source

@[simp]

theorem dfinsupp.comap_domain_apply {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {κ : Type u_1} [Π (i : ι), has_zero (β i)] (h : κ → ι) (hh : function.injective h) (f : Π₀ (i : ι), β i) (k : κ) :

⇑(dfinsupp.comap_domain h hh f) k = ⇑f (h k)

source

@[simp]

theorem dfinsupp.comap_domain_zero {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {κ : Type u_1} [Π (i : ι), has_zero (β i)] (h : κ → ι) (hh : function.injective h) :

dfinsupp.comap_domain h hh 0 = 0

source

@[simp]

theorem dfinsupp.comap_domain_add {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {κ : Type u_1} [Π (i : ι), add_zero_class (β i)] (h : κ → ι) (hh : function.injective h) (f g : Π₀ (i : ι), β i) :

dfinsupp.comap_domain h hh (f + g) = dfinsupp.comap_domain h hh f + dfinsupp.comap_domain h hh g

source

@[simp]

theorem dfinsupp.comap_domain_smul {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : decidable_eq ι] {κ : Type u_1} [monoid γ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), distrib_mul_action γ (β i)] (h : κ → ι) (hh : function.injective h) (r : γ) (f : Π₀ (i : ι), β i) :

dfinsupp.comap_domain h hh (r • f) = r • dfinsupp.comap_domain h hh f

source

@[simp]

theorem dfinsupp.comap_domain_single {ι : Type u} {β : ι → Type v} [dec : decidable_eq ι] {κ : Type u_1} [decidable_eq κ] [Π (i : ι), has_zero (β i)] (h : κ → ι) (hh : function.injective h) (k : κ) (x : β (h k)) :

dfinsupp.comap_domain h hh (dfinsupp.single (h k) x) = dfinsupp.single k x

source

def dfinsupp.comap_domain' {ι : Type u} {β : ι → Type v} {κ : Type u_1} [Π (i : ι), has_zero (β i)] (h : κ → ι) {h' : ι → κ} (hh' : function.left_inverse h' h) (f : Π₀ (i : ι), β i) :

Π₀ (k : κ), β (h k)

A computable version of comap_domain when an explicit left inverse is provided.

Equations

dfinsupp.comap_domain' h hh' f = {to_fun := λ (x : κ), ⇑f (h x), support' := trunc.map (λ (s : {s // ∀ (i : ι), i ∈ s ∨ f.to_fun i = 0}), ⟨multiset.map h' ↑s, _⟩) f.support'}

source

@[simp]

theorem dfinsupp.comap_domain'_apply {ι : Type u} {β : ι → Type v} {κ : Type u_1} [Π (i : ι), has_zero (β i)] (h : κ → ι) {h' : ι → κ} (hh' : function.left_inverse h' h) (f : Π₀ (i : ι), β i) (k : κ) :

⇑(dfinsupp.comap_domain' h hh' f) k = ⇑f (h k)

source

@[simp]

theorem dfinsupp.comap_domain'_zero {ι : Type u} {β : ι → Type v} {κ : Type u_1} [Π (i : ι), has_zero (β i)] (h : κ → ι) {h' : ι → κ} (hh' : function.left_inverse h' h) :

dfinsupp.comap_domain' h hh' 0 = 0

source

@[simp]

theorem dfinsupp.comap_domain'_add {ι : Type u} {β : ι → Type v} {κ : Type u_1} [Π (i : ι), add_zero_class (β i)] (h : κ → ι) {h' : ι → κ} (hh' : function.left_inverse h' h) (f g : Π₀ (i : ι), β i) :

dfinsupp.comap_domain' h hh' (f + g) = dfinsupp.comap_domain' h hh' f + dfinsupp.comap_domain' h hh' g

source

@[simp]

theorem dfinsupp.comap_domain'_smul {ι : Type u} {γ : Type w} {β : ι → Type v} {κ : Type u_1} [monoid γ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), distrib_mul_action γ (β i)] (h : κ → ι) {h' : ι → κ} (hh' : function.left_inverse h' h) (r : γ) (f : Π₀ (i : ι), β i) :

dfinsupp.comap_domain' h hh' (r • f) = r • dfinsupp.comap_domain' h hh' f

source

@[simp]

theorem dfinsupp.comap_domain'_single {ι : Type u} {β : ι → Type v} {κ : Type u_1} [decidable_eq ι] [decidable_eq κ] [Π (i : ι), has_zero (β i)] (h : κ → ι) {h' : ι → κ} (hh' : function.left_inverse h' h) (k : κ) (x : β (h k)) :

dfinsupp.comap_domain' h hh' (dfinsupp.single (h k) x) = dfinsupp.single k x

source

def dfinsupp.equiv_congr_left {ι : Type u} {β : ι → Type v} {κ : Type u_1} [Π (i : ι), has_zero (β i)] (h : ι ≃ κ) :

(Π₀ (i : ι), β i) ≃ Π₀ (k : κ), β (⇑(h.symm) k)

Reindexing terms of a dfinsupp.

This is the dfinsupp version of equiv.Pi_congr_left'.

Equations

dfinsupp.equiv_congr_left h = {to_fun := dfinsupp.comap_domain' ⇑(h.symm) _, inv_fun := λ (f : Π₀ (k : κ), β (⇑(h.symm) k)), dfinsupp.map_range (λ (i : ι), ⇑(equiv.cast _)) _ (dfinsupp.comap_domain' ⇑h _ f), left_inv := _, right_inv := _}

source

@[simp]

theorem dfinsupp.equiv_congr_left_apply {ι : Type u} {β : ι → Type v} {κ : Type u_1} [Π (i : ι), has_zero (β i)] (h : ι ≃ κ) (f : Π₀ (i : ι), (λ (i : ι), β i) i) :

⇑(dfinsupp.equiv_congr_left h) f = dfinsupp.comap_domain' ⇑(h.symm) _ f

source

@[protected, instance]

def dfinsupp.has_add₂ {ι : Type u} {α : ι → Type u_2} {δ : Π (i : ι), α i → Type v} [Π (i : ι) (j : α i), add_zero_class (δ i j)] :

has_add (Π₀ (i : ι) (j : α i), δ i j)

Equations

dfinsupp.has_add₂ = dfinsupp.has_add

source

@[protected, instance]

def dfinsupp.add_zero_class₂ {ι : Type u} {α : ι → Type u_2} {δ : Π (i : ι), α i → Type v} [Π (i : ι) (j : α i), add_zero_class (δ i j)] :

add_zero_class (Π₀ (i : ι) (j : α i), δ i j)

Equations

dfinsupp.add_zero_class₂ = dfinsupp.add_zero_class

source

@[protected, instance]

def dfinsupp.add_monoid₂ {ι : Type u} {α : ι → Type u_2} {δ : Π (i : ι), α i → Type v} [Π (i : ι) (j : α i), add_monoid (δ i j)] :

add_monoid (Π₀ (i : ι) (j : α i), δ i j)

Equations

dfinsupp.add_monoid₂ = dfinsupp.add_monoid

source

@[protected, instance]

def dfinsupp.distrib_mul_action₂ {ι : Type u} {γ : Type w} {α : ι → Type u_2} {δ : Π (i : ι), α i → Type v} [monoid γ] [Π (i : ι) (j : α i), add_monoid (δ i j)] [Π (i : ι) (j : α i), distrib_mul_action γ (δ i j)] :

distrib_mul_action γ (Π₀ (i : ι) (j : α i), δ i j)

Equations

dfinsupp.distrib_mul_action₂ = dfinsupp.distrib_mul_action

source

noncomputable def dfinsupp.sigma_curry {ι : Type u} {α : ι → Type u_2} {δ : Π (i : ι), α i → Type v} [Π (i : ι) (j : α i), has_zero (δ i j)] (f : Π₀ (i : Σ (i : ι), α i), δ i.fst i.snd) :

Π₀ (i : ι) (j : α i), δ i j

The natural map between Π₀ (i : Σ i, α i), δ i.1 i.2 and Π₀ i (j : α i), δ i j.

Equations

f.sigma_curry = dfinsupp.mk (finset.image (λ (i : Σ (i : ι), α i), i.fst) f.support) (λ (i : ↥↑(finset.image (λ (i : Σ (i : ι), α i), i.fst) f.support)), dfinsupp.mk (f.support.preimage (sigma.mk ↑i) _) (λ (j : ↥↑(f.support.preimage (sigma.mk ↑i) _)), ⇑f ⟨↑i, ↑j⟩))

source

@[simp]

theorem dfinsupp.sigma_curry_apply {ι : Type u} {α : ι → Type u_2} {δ : Π (i : ι), α i → Type v} [Π (i : ι) (j : α i), has_zero (δ i j)] (f : Π₀ (i : Σ (i : ι), α i), δ i.fst i.snd) (i : ι) (j : α i) :

⇑(⇑(f.sigma_curry) i) j = ⇑f ⟨i, j⟩

source

@[simp]

theorem dfinsupp.sigma_curry_zero {ι : Type u} {α : ι → Type u_2} {δ : Π (i : ι), α i → Type v} [Π (i : ι) (j : α i), has_zero (δ i j)] :

0.sigma_curry = 0

source

@[simp]

theorem dfinsupp.sigma_curry_add {ι : Type u} {α : ι → Type u_2} {δ : Π (i : ι), α i → Type v} [Π (i : ι) (j : α i), add_zero_class (δ i j)] (f g : Π₀ (i : Σ (i : ι), α i), δ i.fst i.snd) :

(f + g).sigma_curry = f.sigma_curry + g.sigma_curry

source

@[simp]

theorem dfinsupp.sigma_curry_smul {ι : Type u} {γ : Type w} {α : ι → Type u_2} {δ : Π (i : ι), α i → Type v} [monoid γ] [Π (i : ι) (j : α i), add_monoid (δ i j)] [Π (i : ι) (j : α i), distrib_mul_action γ (δ i j)] (r : γ) (f : Π₀ (i : Σ (i : ι), α i), δ i.fst i.snd) :

(r • f).sigma_curry = r • f.sigma_curry

source

@[simp]

theorem dfinsupp.sigma_curry_single {ι : Type u} {α : ι → Type u_2} {δ : Π (i : ι), α i → Type v} [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι) (j : α i), has_zero (δ i j)] (ij : Σ (i : ι), α i) (x : δ ij.fst ij.snd) :

(dfinsupp.single ij x).sigma_curry = dfinsupp.single ij.fst (dfinsupp.single ij.snd x)

source

def dfinsupp.sigma_uncurry {ι : Type u} {α : ι → Type u_2} {δ : Π (i : ι), α i → Type v} [Π (i : ι) (j : α i), has_zero (δ i j)] [Π (i : ι), decidable_eq (α i)] [Π (i : ι) (j : α i) (x : δ i j), decidable (x ≠ 0)] (f : Π₀ (i : ι) (j : α i), δ i j) :

Π₀ (i : Σ (i : ι), α i), δ i.fst i.snd

The natural map between Π₀ i (j : α i), δ i j and Π₀ (i : Σ i, α i), δ i.1 i.2, inverse of curry.

Equations

f.sigma_uncurry = {to_fun := λ (i : Σ (i : ι), α i), ⇑(⇑f i.fst) i.snd, support' := trunc.map (λ (s : {s // ∀ (i : ι), i ∈ s ∨ f.to_fun i = 0}), ⟨↑s.bind (λ (i : ι), (finset.map {to_fun := sigma.mk i, inj' := _} (⇑f i).support).val), _⟩) f.support'}

source

@[simp]

theorem dfinsupp.sigma_uncurry_apply {ι : Type u} {α : ι → Type u_2} {δ : Π (i : ι), α i → Type v} [Π (i : ι) (j : α i), has_zero (δ i j)] [Π (i : ι), decidable_eq (α i)] [Π (i : ι) (j : α i) (x : δ i j), decidable (x ≠ 0)] (f : Π₀ (i : ι) (j : α i), δ i j) (i : ι) (j : α i) :

⇑(f.sigma_uncurry) ⟨i, j⟩ = ⇑(⇑f i) j

source

@[simp]

theorem dfinsupp.sigma_uncurry_zero {ι : Type u} {α : ι → Type u_2} {δ : Π (i : ι), α i → Type v} [Π (i : ι) (j : α i), has_zero (δ i j)] [Π (i : ι), decidable_eq (α i)] [Π (i : ι) (j : α i) (x : δ i j), decidable (x ≠ 0)] :

0.sigma_uncurry = 0

source

@[simp]

theorem dfinsupp.sigma_uncurry_add {ι : Type u} {α : ι → Type u_2} {δ : Π (i : ι), α i → Type v} [Π (i : ι) (j : α i), add_zero_class (δ i j)] [Π (i : ι), decidable_eq (α i)] [Π (i : ι) (j : α i) (x : δ i j), decidable (x ≠ 0)] (f g : Π₀ (i : ι) (j : α i), δ i j) :

(f + g).sigma_uncurry = f.sigma_uncurry + g.sigma_uncurry

source

@[simp]

theorem dfinsupp.sigma_uncurry_smul {ι : Type u} {γ : Type w} {α : ι → Type u_2} {δ : Π (i : ι), α i → Type v} [monoid γ] [Π (i : ι) (j : α i), add_monoid (δ i j)] [Π (i : ι), decidable_eq (α i)] [Π (i : ι) (j : α i) (x : δ i j), decidable (x ≠ 0)] [Π (i : ι) (j : α i), distrib_mul_action γ (δ i j)] (r : γ) (f : Π₀ (i : ι) (j : α i), δ i j) :

(r • f).sigma_uncurry = r • f.sigma_uncurry

source

@[simp]

theorem dfinsupp.sigma_uncurry_single {ι : Type u} {α : ι → Type u_2} {δ : Π (i : ι), α i → Type v} [Π (i : ι) (j : α i), has_zero (δ i j)] [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι) (j : α i) (x : δ i j), decidable (x ≠ 0)] (i : ι) (j : α i) (x : δ i j) :

(dfinsupp.single i (dfinsupp.single j x)).sigma_uncurry = dfinsupp.single ⟨i, j⟩ x

source

noncomputable def dfinsupp.sigma_curry_equiv {ι : Type u} {α : ι → Type u_2} {δ : Π (i : ι), α i → Type v} [Π (i : ι) (j : α i), has_zero (δ i j)] [Π (i : ι), decidable_eq (α i)] [Π (i : ι) (j : α i) (x : δ i j), decidable (x ≠ 0)] :

(Π₀ (i : Σ (i : ι), α i), δ i.fst i.snd) ≃ Π₀ (i : ι) (j : α i), δ i j

The natural bijection between Π₀ (i : Σ i, α i), δ i.1 i.2 and Π₀ i (j : α i), δ i j.

This is the dfinsupp version of equiv.Pi_curry.

Equations

dfinsupp.sigma_curry_equiv = {to_fun := dfinsupp.sigma_curry _inst_1, inv_fun := dfinsupp.sigma_uncurry (λ (i : ι) (j : α i) (x : δ i j), _inst_3 i j x), left_inv := _, right_inv := _}

source

def dfinsupp.extend_with {ι : Type u} {α : option ι → Type v} [Π (i : option ι), has_zero (α i)] (a : α option.none) (f : Π₀ (i : ι), α (option.some i)) :

Π₀ (i : option ι), α i

Adds a term to a dfinsupp, making a dfinsupp indexed by an option.

This is the dfinsupp version of option.rec.

Equations

dfinsupp.extend_with a f = {to_fun := option.rec a ⇑f, support' := trunc.map (λ (s : {s // ∀ (i : ι), i ∈ s ∨ f.to_fun i = 0}), ⟨option.none ::ₘ multiset.map option.some ↑s, _⟩) f.support'}

source

@[simp]

theorem dfinsupp.extend_with_none {ι : Type u} {α : option ι → Type v} [Π (i : option ι), has_zero (α i)] (f : Π₀ (i : ι), α (option.some i)) (a : α option.none) :

⇑(dfinsupp.extend_with a f) option.none = a

source

@[simp]

theorem dfinsupp.extend_with_some {ι : Type u} {α : option ι → Type v} [Π (i : option ι), has_zero (α i)] (f : Π₀ (i : ι), α (option.some i)) (a : α option.none) (i : ι) :

⇑(dfinsupp.extend_with a f) (option.some i) = ⇑f i

source

@[simp]

theorem dfinsupp.extend_with_single_zero {ι : Type u} {α : option ι → Type v} [decidable_eq ι] [Π (i : option ι), has_zero (α i)] (i : ι) (x : α (option.some i)) :

dfinsupp.extend_with 0 (dfinsupp.single i x) = dfinsupp.single (option.some i) x

source

@[simp]

theorem dfinsupp.extend_with_zero {ι : Type u} {α : option ι → Type v} [decidable_eq ι] [Π (i : option ι), has_zero (α i)] (x : α option.none) :

dfinsupp.extend_with x 0 = dfinsupp.single option.none x

source

@[simp]

theorem dfinsupp.equiv_prod_dfinsupp_symm_apply {ι : Type u} [dec : decidable_eq ι] {α : option ι → Type v} [Π (i : option ι), has_zero (α i)] (f : α option.none × Π₀ (i : ι), α (option.some i)) :

⇑(dfinsupp.equiv_prod_dfinsupp.symm) f = dfinsupp.extend_with f.fst f.snd

source

noncomputable def dfinsupp.equiv_prod_dfinsupp {ι : Type u} [dec : decidable_eq ι] {α : option ι → Type v} [Π (i : option ι), has_zero (α i)] :

(Π₀ (i : option ι), α i) ≃ α option.none × Π₀ (i : ι), α (option.some i)

Bijection obtained by separating the term of index none of a dfinsupp over option ι.

This is the dfinsupp version of equiv.pi_option_equiv_prod.

Equations

dfinsupp.equiv_prod_dfinsupp = {to_fun := λ (f : Π₀ (i : option ι), α i), (⇑f option.none, dfinsupp.comap_domain option.some _ f), inv_fun := λ (f : α option.none × Π₀ (i : ι), α (option.some i)), dfinsupp.extend_with f.fst f.snd, left_inv := _, right_inv := _}

source

@[simp]

theorem dfinsupp.equiv_prod_dfinsupp_apply {ι : Type u} [dec : decidable_eq ι] {α : option ι → Type v} [Π (i : option ι), has_zero (α i)] (f : Π₀ (i : option ι), α i) :

⇑dfinsupp.equiv_prod_dfinsupp f = (⇑f option.none, dfinsupp.comap_domain option.some _ f)

source

theorem dfinsupp.equiv_prod_dfinsupp_add {ι : Type u} [dec : decidable_eq ι] {α : option ι → Type v} [Π (i : option ι), add_zero_class (α i)] (f g : Π₀ (i : option ι), α i) :

⇑dfinsupp.equiv_prod_dfinsupp (f + g) = ⇑dfinsupp.equiv_prod_dfinsupp f + ⇑dfinsupp.equiv_prod_dfinsupp g

source

theorem dfinsupp.equiv_prod_dfinsupp_smul {ι : Type u} {γ : Type w} [dec : decidable_eq ι] {α : option ι → Type v} [monoid γ] [Π (i : option ι), add_monoid (α i)] [Π (i : option ι), distrib_mul_action γ (α i)] (r : γ) (f : Π₀ (i : option ι), α i) :

⇑dfinsupp.equiv_prod_dfinsupp (r • f) = r • ⇑dfinsupp.equiv_prod_dfinsupp f

source

def dfinsupp.prod {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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

f.prod g = f.support.prod (λ (i : ι), g i (⇑f i))

source

def dfinsupp.sum {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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

f.sum g = f.support.sum (λ (i : ι), g i (⇑f i))

source

theorem dfinsupp.sum_map_range_index {ι : Type u} {γ : Type w} [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)] [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} {γ : Type w} [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)] [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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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_eq_zero {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] [add_comm_monoid γ] {f : Π₀ (i : ι), β i} {h : Π (i : ι), β i → γ} (hyp : ∀ (i : ι), h i (⇑f i) = 0) :

f.sum h = 0

source

theorem dfinsupp.prod_eq_one {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] [comm_monoid γ] {f : Π₀ (i : ι), β i} {h : Π (i : ι), β i → γ} (hyp : ∀ (i : ι), h i (⇑f i) = 1) :

f.prod h = 1

source

theorem dfinsupp.smul_sum {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : decidable_eq ι] {α : Type u_1} [monoid α] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] [add_comm_monoid γ] [distrib_mul_action α γ] {f : Π₀ (i : ι), β i} {h : Π (i : ι), β i → γ} {c : α} :

c • f.sum h = f.sum (λ (a : ι) (b : β a), c • h a b)

source

theorem dfinsupp.sum_add_index {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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

theorem dfinsupp_prod_mem {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] [comm_monoid γ] {S : Type u_1} [set_like S γ] [submonoid_class S γ] (s : S) (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i → γ) (h : ∀ (c : ι), ⇑f c ≠ 0 → g c (⇑f c) ∈ s) :

f.prod g ∈ s

source

theorem dfinsupp_sum_mem {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] [add_comm_monoid γ] {S : Type u_1} [set_like S γ] [add_submonoid_class S γ] (s : S) (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i → γ) (h : ∀ (c : ι), ⇑f c ≠ 0 → g c (⇑f c) ∈ s) :

f.sum g ∈ s

source

@[simp]

theorem dfinsupp.sum_eq_sum_fintype {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : decidable_eq ι] [fintype ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] [add_comm_monoid γ] (v : Π₀ (i : ι), β i) [f : Π (i : ι), β i → γ] (hf : ∀ (i : ι), f i 0 = 0) :

v.sum f = finset.univ.sum (λ (i : ι), f i (⇑dfinsupp.equiv_fun_on_fintype v i))

source

@[simp]

theorem dfinsupp.prod_eq_prod_fintype {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : decidable_eq ι] [fintype ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x ≠ 0)] [comm_monoid γ] (v : Π₀ (i : ι), β i) [f : Π (i : ι), β i → γ] (hf : ∀ (i : ι), f i 0 = 1) :

v.prod f = finset.univ.prod (λ (i : ι), f i (⇑dfinsupp.equiv_fun_on_fintype v i))

source

def dfinsupp.sum_add_hom {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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

dfinsupp.sum_add_hom φ = {to_fun := λ (f : Π₀ (i : ι), β i), trunc.lift (λ (s : {s // ∀ (i : ι), i ∈ s ∨ f.to_fun i = 0}), ↑s.to_finset.sum (λ (i : ι), ⇑(φ i) (⇑f i))) _ f.support', map_zero' := _, map_add' := _}

source

@[simp]

theorem dfinsupp.sum_add_hom_single {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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_mem {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] [add_comm_monoid γ] {S : Type u_1} [set_like S γ] [add_submonoid_class S γ] (s : S) (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i →+ γ) (h : ∀ (c : ι), ⇑f c ≠ 0 → ⇑(g c) (⇑f c) ∈ s) :

⇑(dfinsupp.sum_add_hom g) f ∈ s

source

theorem add_submonoid.supr_eq_mrange_dfinsupp_sum_add_hom {ι : Type u} {γ : Type w} [dec : decidable_eq ι] [add_comm_monoid γ] (S : ι → add_submonoid γ) :

supr S = add_monoid_hom.mrange (dfinsupp.sum_add_hom (λ (i : ι), (S i).subtype))

The supremum of a family of commutative additive submonoids is equal to the range of dfinsupp.sum_add_hom; that is, every element in the supr can be produced from taking a finite number of non-zero elements of S i, coercing them to γ, and summing them.

source

theorem add_submonoid.bsupr_eq_mrange_dfinsupp_sum_add_hom {ι : Type u} {γ : Type w} [dec : decidable_eq ι] (p : ι → Prop) [decidable_pred p] [add_comm_monoid γ] (S : ι → add_submonoid γ) :

(⨆ (i : ι) (h : p i), S i) = add_monoid_hom.mrange ((dfinsupp.sum_add_hom (λ (i : ι), (S i).subtype)).comp (dfinsupp.filter_add_monoid_hom (λ (i : ι), ↥(S i)) p))

The bounded supremum of a family of commutative additive submonoids is equal to the range of dfinsupp.sum_add_hom composed with dfinsupp.filter_add_monoid_hom; that is, every element in the bounded supr can be produced from taking a finite number of non-zero elements from the S i that satisfy p i, coercing them to γ, and summing them.

source

theorem add_submonoid.mem_supr_iff_exists_dfinsupp {ι : Type u} {γ : Type w} [dec : decidable_eq ι] [add_comm_monoid γ] (S : ι → add_submonoid γ) (x : γ) :

x ∈ supr S ↔ ∃ (f : Π₀ (i : ι), ↥(S i)), ⇑(dfinsupp.sum_add_hom (λ (i : ι), (S i).subtype)) f = x

source

theorem add_submonoid.mem_supr_iff_exists_dfinsupp' {ι : Type u} {γ : Type w} [dec : decidable_eq ι] [add_comm_monoid γ] (S : ι → add_submonoid γ) [Π (i : ι) (x : ↥(S i)), decidable (x ≠ 0)] (x : γ) :

x ∈ supr S ↔ ∃ (f : Π₀ (i : ι), ↥(S i)), f.sum (λ (i : ι) (xi : ↥(S i)), ↑xi) = x

A variant of add_submonoid.mem_supr_iff_exists_dfinsupp with the RHS fully unfolded.

source

theorem add_submonoid.mem_bsupr_iff_exists_dfinsupp {ι : Type u} {γ : Type w} [dec : decidable_eq ι] (p : ι → Prop) [decidable_pred p] [add_comm_monoid γ] (S : ι → add_submonoid γ) (x : γ) :

(x ∈ ⨆ (i : ι) (h : p i), S i) ↔ ∃ (f : Π₀ (i : ι), ↥(S i)), ⇑(dfinsupp.sum_add_hom (λ (i : ι), (S i).subtype)) (dfinsupp.filter p f) = x

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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] [add_comm_monoid γ] :

(Π (i : ι), β i →+ γ) ≃+ ((Π₀ (i : ι), β i) →+ γ)

The dfinsupp version of finsupp.lift_add_hom,

Equations

dfinsupp.lift_add_hom = {to_fun := dfinsupp.sum_add_hom _inst_2, inv_fun := λ (F : (Π₀ (i : ι), β i) →+ γ) (i : ι), F.comp (dfinsupp.single_add_hom β i), left_inv := _, right_inv := _, map_add' := _}

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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] {δ : 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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] {δ : 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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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₂) :

s.prod (λ (i : α), (g i).prod h) = (s.sum (λ (i : α), 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₂) :

s.sum (λ (i : α), (g i).sum h) = (s.sum (λ (i : α), g i)).sum h

source

theorem dfinsupp.sum_sum_index {ι : Type u} {γ : Type w} {β : ι → 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)] [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 w} {β : ι → 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)] [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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [dec : decidable_eq ι] [Π (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 w} {β : ι → Type v} [Π (i : ι), add_comm_monoid (β i)] {s : finset γ} {h : γ → (Π₀ (i : ι), β i)} {p : ι → Prop} [decidable_pred p] :

dfinsupp.subtype_domain p (s.sum (λ (c : γ), h c)) = s.sum (λ (c : γ), dfinsupp.subtype_domain p (h c))

source

theorem dfinsupp.subtype_domain_finsupp_sum {ι : Type u} {γ : Type w} {β : ι → Type v} {δ : γ → 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))

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) (x : Π₀ (i : ι), (λ (i : ι), β₁ i) i) :

⇑(dfinsupp.map_range.add_monoid_hom f) x = dfinsupp.map_range (λ (i : ι) (x : β₁ i), ⇑(f i) x) _ x

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

dfinsupp.map_range.add_monoid_hom f = {to_fun := dfinsupp.map_range (λ (i : ι) (x : β₁ i), ⇑(f i) x) _, map_zero' := _, map_add' := _}

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

dfinsupp.map_range.add_equiv e = {to_fun := dfinsupp.map_range (λ (i : ι) (x : β₁ i), ⇑(e i) x) _, inv_fun := dfinsupp.map_range (λ (i : ι) (x : β₂ i), ⇑((e i).symm) x) _, left_inv := _, right_inv := _, map_add' := _}

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) (x : Π₀ (i : ι), (λ (i : ι), β₁ i) i) :

⇑(dfinsupp.map_range.add_equiv e) x = dfinsupp.map_range (λ (i : ι) (x : β₁ i), ⇑(e i) x) _ x

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)

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)

source

@[simp]

theorem ring_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_semiring R] [comm_semiring 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

@[simp]

theorem ring_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)] [non_assoc_semiring R] [non_assoc_semiring 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 add_equiv.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 mul_equiv.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

@[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_zero_class (β 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_zero_class (β 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_zero_class (β 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

source

@[simp]

theorem ring_hom.map_dfinsupp_sum_add_hom {ι : Type u} {β : ι → Type v} [decidable_eq ι] {R : Type u_1} {S : Type u_2} [non_assoc_semiring R] [non_assoc_semiring S] [Π (i : ι), add_zero_class (β i)] (h : R →+* S) (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i →+ R) :

⇑h (⇑(dfinsupp.sum_add_hom g) f) = ⇑(dfinsupp.sum_add_hom (λ (i : ι), h.to_add_monoid_hom.comp (g i))) f

source

@[simp]

theorem add_equiv.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_zero_class (β i)] (h : R ≃+ S) (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i →+ R) :

⇑h (⇑(dfinsupp.sum_add_hom g) f) = ⇑(dfinsupp.sum_add_hom (λ (i : ι), h.to_add_monoid_hom.comp (g i))) f

source

@[protected, instance]

def dfinsupp.fintype {ι : Type u_1} {π : ι → Type u_2} [decidable_eq ι] [Π (i : ι), has_zero (π i)] [fintype ι] [Π (i : ι), fintype (π i)] :

fintype (Π₀ (i : ι), π i)

Equations

dfinsupp.fintype = fintype.of_equiv (Π (i : ι), π i) dfinsupp.equiv_fun_on_fintype.symm

source

@[protected, instance]

def dfinsupp.infinite_of_left {ι : Type u_1} {π : ι → Type u_2} [∀ (i : ι), nontrivial (π i)] [Π (i : ι), has_zero (π i)] [infinite ι] :

infinite (Π₀ (i : ι), π i)

source

theorem dfinsupp.infinite_of_exists_right {ι : Type u_1} {π : ι → Type u_2} (i : ι) [infinite (π i)] [Π (i : ι), has_zero (π i)] :

infinite (Π₀ (i : ι), π i)

See dfinsupp.infinite_of_right for this in instance form, with the drawback that it needs all π i to be infinite.

source

@[protected, instance]

def dfinsupp.infinite_of_right {ι : Type u_1} {π : ι → Type u_2} [∀ (i : ι), infinite (π i)] [Π (i : ι), has_zero (π i)] [nonempty ι] :

infinite (Π₀ (i : ι), π i)

See dfinsupp.infinite_of_exists_right for the case that only one π ι is infinite.

mathlib3 documentation

Dependent functions with finite support #

Notation #

Implementation notes #

Bundled versions of `dfinsupp.map_range` #

Product and sum lemmas for bundled morphisms. #

Dependent functions with finite support #

Notation #

Implementation notes #

Bundled versions of dfinsupp.map_range #

Product and sum lemmas for bundled morphisms. #

Bundled versions of `dfinsupp.map_range` #