# mathlib3documentation

data.dfinsupp.basic

# Dependent functions with finite support #

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

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

## Notation #

This file introduces the notation Π₀ a, β a as notation for dfinsupp β, mirroring the α →₀ β notation used for finsupp. This works for nested binders too, with Π₀ a b, γ a b as notation for dfinsupp (λ a, dfinsupp (γ a)).

## Implementation notes #

The support is internally represented (in the primed dfinsupp.support') as a multiset that represents a superset of the true support of the function, quotiented by the always-true relation so that this does not impact equality. This approach has computational benefits over storing a finset; it allows us to add together two finitely-supported functions (dfinsupp.has_add) without having to evaluate the resulting function to recompute its support (which would required decidability of b = 0 for b : β i).

The true support of the function can still be recovered with dfinsupp.support; but these decidability obligations are now postponed to when the support is actually needed. As a consequence, there are two ways to sum a dfinsupp: with dfinsupp.sum which works over an arbitrary function but requires recomputation of the support and therefore a decidable argument; and with dfinsupp.sum_add_hom which requires an additive morphism, using its properties to show that summing over a superset of the support is sufficient.

finsupp takes an altogether different approach here; it uses classical.decidable and declares finsupp.has_add as noncomputable. This design difference is independent of the fact that dfinsupp is dependently-typed and finsupp is not; in future, we may want to align these two definitions, or introduce two more definitions for the other combinations of decisions.

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

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
@[protected, instance]
def dfinsupp.fun_like {ι : Type u} {β : ι Type v} [Π (i : ι), has_zero (β i)] :
fun_like (Π₀ (i : ι), β i) ι β
Equations
@[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
@[simp]
theorem dfinsupp.to_fun_eq_coe {ι : Type u} {β : ι Type v} [Π (i : ι), has_zero (β i)] (f : Π₀ (i : ι), β i) :
@[ext]
theorem dfinsupp.ext {ι : Type u} {β : ι Type v} [Π (i : ι), has_zero (β i)] {f g : Π₀ (i : ι), β i} (h : (i : ι), f i = g i) :
f = g
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.

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

Deprecated. Use fun_like.coe_injective instead.

@[protected, instance]
def dfinsupp.has_zero {ι : Type u} {β : ι Type v} [Π (i : ι), has_zero (β i)] :
has_zero (Π₀ (i : ι), β i)
Equations
@[protected, instance]
def dfinsupp.inhabited {ι : Type u} {β : ι Type v} [Π (i : ι), has_zero (β i)] :
inhabited (Π₀ (i : ι), β i)
Equations
@[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
@[simp]
theorem dfinsupp.coe_zero {ι : Type u} {β : ι Type v} [Π (i : ι), has_zero (β i)] :
0 = 0
theorem dfinsupp.zero_apply {ι : Type u} {β : ι Type v} [Π (i : ι), has_zero (β i)] (i : ι) :
0 i = 0
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:

• dfinsupp.map_range.add_monoid_hom
• dfinsupp.map_range.add_equiv
• dfinsupp.map_range.linear_map
• dfinsupp.map_range.linear_equiv
Equations
@[simp]
theorem dfinsupp.map_range_apply {ι : Type u} {β₁ : ι Type v₁} {β₂ : ι Type v₂} [Π (i : ι), has_zero (β₁ i)] [Π (i : ι), has_zero (β₂ i)] (f : Π (i : ι), β₁ i β₂ i) (hf : (i : ι), f i 0 = 0) (g : Π₀ (i : ι), β₁ i) (i : ι) :
hf g) i = f i (g i)
@[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
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 = hf₂ g)
@[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) :
0 = 0
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
@[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 : ι) :
hf g₁ g₂) i = f i (g₁ i) (g₂ i)
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
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)
@[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)] :
@[protected, instance]
def dfinsupp.has_add {ι : Type u} {β : ι Type v} [Π (i : ι), add_zero_class (β i)] :
has_add (Π₀ (i : ι), β i)
Equations
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
@[simp]
theorem dfinsupp.coe_add {ι : Type u} {β : ι Type v} [Π (i : ι), add_zero_class (β i)] (g₁ g₂ : Π₀ (i : ι), β i) :
(g₁ + g₂) = g₁ + g₂
@[protected, instance]
def dfinsupp.add_zero_class {ι : Type u} {β : ι Type v} [Π (i : ι), add_zero_class (β i)] :
add_zero_class (Π₀ (i : ι), β i)
Equations
@[protected, instance]
def dfinsupp.has_nat_scalar {ι : Type u} {β : ι Type v} [Π (i : ι), add_monoid (β i)] :
(Π₀ (i : ι), β i)

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

Equations
theorem dfinsupp.nsmul_apply {ι : Type u} {β : ι Type v} [Π (i : ι), add_monoid (β i)] (b : ) (v : Π₀ (i : ι), β i) (i : ι) :
(b v) i = b v i
@[simp]
theorem dfinsupp.coe_nsmul {ι : Type u} {β : ι Type v} [Π (i : ι), add_monoid (β i)] (b : ) (v : Π₀ (i : ι), β i) :
(b v) = b v
@[protected, instance]
def dfinsupp.add_monoid {ι : Type u} {β : ι Type v} [Π (i : ι), add_monoid (β i)] :
add_monoid (Π₀ (i : ι), β i)
Equations
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
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
@[protected, instance]
def dfinsupp.add_comm_monoid {ι : Type u} {β : ι Type v} [Π (i : ι), add_comm_monoid (β i)] :
add_comm_monoid (Π₀ (i : ι), β i)
Equations
@[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))
@[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)
@[protected, instance]
def dfinsupp.has_neg {ι : Type u} {β : ι Type v} [Π (i : ι), add_group (β i)] :
has_neg (Π₀ (i : ι), β i)
Equations
theorem dfinsupp.neg_apply {ι : Type u} {β : ι Type v} [Π (i : ι), add_group (β i)] (g : Π₀ (i : ι), β i) (i : ι) :
(-g) i = -g i
@[simp]
theorem dfinsupp.coe_neg {ι : Type u} {β : ι Type v} [Π (i : ι), add_group (β i)] (g : Π₀ (i : ι), β i) :
@[protected, instance]
def dfinsupp.has_sub {ι : Type u} {β : ι Type v} [Π (i : ι), add_group (β i)] :
has_sub (Π₀ (i : ι), β i)
Equations
theorem dfinsupp.sub_apply {ι : Type u} {β : ι Type v} [Π (i : ι), add_group (β i)] (g₁ g₂ : Π₀ (i : ι), β i) (i : ι) :
(g₁ - g₂) i = g₁ i - g₂ i
@[simp]
theorem dfinsupp.coe_sub {ι : Type u} {β : ι Type v} [Π (i : ι), add_group (β i)] (g₁ g₂ : Π₀ (i : ι), β i) :
(g₁ - g₂) = g₁ - g₂
@[protected, instance]
def dfinsupp.has_int_scalar {ι : Type u} {β : ι Type v} [Π (i : ι), add_group (β i)] :
(Π₀ (i : ι), β i)

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

Equations
theorem dfinsupp.zsmul_apply {ι : Type u} {β : ι Type v} [Π (i : ι), add_group (β i)] (b : ) (v : Π₀ (i : ι), β i) (i : ι) :
(b v) i = b v i
@[simp]
theorem dfinsupp.coe_zsmul {ι : Type u} {β : ι Type v} [Π (i : ι), add_group (β i)] (b : ) (v : Π₀ (i : ι), β i) :
(b v) = b v
@[protected, instance]
def dfinsupp.add_group {ι : Type u} {β : ι Type v} [Π (i : ι), add_group (β i)] :
add_group (Π₀ (i : ι), β i)
Equations
@[protected, instance]
def dfinsupp.add_comm_group {ι : Type u} {β : ι Type v} [Π (i : ι), add_comm_group (β i)] :
add_comm_group (Π₀ (i : ι), β i)
Equations
@[protected, instance]
def dfinsupp.has_smul {ι : Type u} {γ : Type w} {β : ι Type v} [monoid γ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), (β i)] :
(Π₀ (i : ι), β i)

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

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

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

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

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

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

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

Equations
@[simp]
theorem dfinsupp.filter_apply {ι : Type u} {β : ι Type v} [Π (i : ι), has_zero (β i)] (p : ι Prop) (i : ι) (f : Π₀ (i : ι), β i) :
f) i = ite (p i) (f i) 0
theorem dfinsupp.filter_apply_pos {ι : Type u} {β : ι Type v} [Π (i : ι), has_zero (β i)] {p : ι Prop} (f : Π₀ (i : ι), β i) {i : ι} (h : p i) :
f) i = f i
theorem dfinsupp.filter_apply_neg {ι : Type u} {β : ι Type v} [Π (i : ι), has_zero (β i)] {p : ι Prop} (f : Π₀ (i : ι), β i) {i : ι} (h : ¬p i) :
f) i = 0
theorem dfinsupp.filter_pos_add_filter_neg {ι : Type u} {β : ι Type v} [Π (i : ι), add_zero_class (β i)] (f : Π₀ (i : ι), β i) (p : ι Prop)  :
+ dfinsupp.filter (λ (i : ι), ¬p i) f = f
@[simp]
theorem dfinsupp.filter_zero {ι : Type u} {β : ι Type v} [Π (i : ι), has_zero (β i)] (p : ι Prop)  :
= 0
@[simp]
theorem dfinsupp.filter_add {ι : Type u} {β : ι Type v} [Π (i : ι), add_zero_class (β i)] (p : ι Prop) (f g : Π₀ (i : ι), β i) :
(f + g) = +
@[simp]
theorem dfinsupp.filter_smul {ι : Type u} {γ : Type w} {β : ι Type v} [monoid γ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), (β i)] (p : ι Prop) (r : γ) (f : Π₀ (i : ι), β i) :
(r f) = r
def dfinsupp.filter_add_monoid_hom {ι : Type u} (β : ι Type v) [Π (i : ι), add_zero_class (β i)] (p : ι Prop)  :
(Π₀ (i : ι), β i) →+ Π₀ (i : ι), β i

dfinsupp.filter as an add_monoid_hom.

Equations
@[simp]
theorem dfinsupp.filter_add_monoid_hom_apply {ι : Type u} (β : ι Type v) [Π (i : ι), add_zero_class (β i)] (p : ι Prop) (x : Π₀ (i : ι), (λ (i : ι), β i) i) :
=
@[simp]
theorem dfinsupp.filter_linear_map_apply {ι : Type u} (γ : Type w) (β : ι Type v) [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), (β i)] (p : ι Prop) (x : Π₀ (i : ι), (λ (i : ι), β i) i) :
p) x =
def dfinsupp.filter_linear_map {ι : Type u} (γ : Type w) (β : ι Type v) [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), (β i)] (p : ι Prop)  :
(Π₀ (i : ι), β i) →ₗ[γ] Π₀ (i : ι), β i

dfinsupp.filter as a linear_map.

Equations
@[simp]
theorem dfinsupp.filter_neg {ι : Type u} {β : ι Type v} [Π (i : ι), add_group (β i)] (p : ι Prop) (f : Π₀ (i : ι), β i) :
(-f) = -
@[simp]
theorem dfinsupp.filter_sub {ι : Type u} {β : ι Type v} [Π (i : ι), add_group (β i)] (p : ι Prop) (f g : Π₀ (i : ι), β i) :
(f - g) = -
def dfinsupp.subtype_domain {ι : Type u} {β : ι Type v} [Π (i : ι), has_zero (β i)] (p : ι Prop) (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
@[simp]
theorem dfinsupp.subtype_domain_zero {ι : Type u} {β : ι Type v} [Π (i : ι), has_zero (β i)] {p : ι Prop}  :
@[simp]
theorem dfinsupp.subtype_domain_apply {ι : Type u} {β : ι Type v} [Π (i : ι), has_zero (β i)] {p : ι Prop} {i : subtype p} {v : Π₀ (i : ι), β i} :
i = v i
@[simp]
theorem dfinsupp.subtype_domain_add {ι : Type u} {β : ι Type v} [Π (i : ι), add_zero_class (β i)] {p : ι Prop} (v v' : Π₀ (i : ι), β i) :
(v + v') =
@[simp]
theorem dfinsupp.subtype_domain_smul {ι : Type u} {γ : Type w} {β : ι Type v} [monoid γ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), (β i)] {p : ι Prop} (r : γ) (f : Π₀ (i : ι), β i) :
(r f) =
def dfinsupp.subtype_domain_add_monoid_hom {ι : Type u} (β : ι Type v) [Π (i : ι), add_zero_class (β i)] (p : ι Prop)  :
(Π₀ (i : ι), β i) →+ Π₀ (i : subtype p), β i

subtype_domain but as an add_monoid_hom.

Equations
@[simp]
theorem dfinsupp.subtype_domain_add_monoid_hom_apply {ι : Type u} (β : ι Type v) [Π (i : ι), add_zero_class (β i)] (p : ι Prop) (x : Π₀ (i : ι), (λ (i : ι), β i) i) :
def dfinsupp.subtype_domain_linear_map {ι : Type u} (γ : Type w) (β : ι Type v) [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), (β i)] (p : ι Prop)  :
(Π₀ (i : ι), β i) →ₗ[γ] Π₀ (i : subtype p), β i

dfinsupp.subtype_domain as a linear_map.

Equations
@[simp]
theorem dfinsupp.subtype_domain_linear_map_apply {ι : Type u} (γ : Type w) (β : ι Type v) [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), (β i)] (p : ι Prop) (x : Π₀ (i : ι), (λ (i : ι), β i) i) :
@[simp]
theorem dfinsupp.subtype_domain_neg {ι : Type u} {β : ι Type v} [Π (i : ι), add_group (β i)] {p : ι Prop} {v : Π₀ (i : ι), β i} :
@[simp]
theorem dfinsupp.subtype_domain_sub {ι : Type u} {β : ι Type v} [Π (i : ι), add_group (β i)] {p : ι Prop} {v v' : Π₀ (i : ι), β i} :
(v - v') =
theorem dfinsupp.finite_support {ι : Type u} {β : ι Type v} [Π (i : ι), has_zero (β i)] (f : Π₀ (i : ι), β i) :
{i : ι | f i 0}.finite
def dfinsupp.mk {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] (s : finset ι) (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
@[simp]
theorem dfinsupp.mk_apply {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {s : finset ι} {x : Π (i : s), β i} {i : ι} :
x) i = dite (i s) (λ (H : i s), x i, H⟩) (λ (H : i s), 0)
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) :
x) i = x i, hi⟩
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) :
x) i = 0
theorem dfinsupp.mk_injective {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] (s : finset ι) :
@[protected, instance]
def dfinsupp.unique {ι : Type u} {β : ι Type v} [Π (i : ι), has_zero (β i)] [ (i : ι), subsingleton (β i)] :
unique (Π₀ (i : ι), β i)
Equations
@[protected, instance]
def dfinsupp.unique_of_is_empty {ι : Type u} {β : ι Type v} [Π (i : ι), has_zero (β i)] [is_empty ι] :
unique (Π₀ (i : ι), β i)
Equations
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
@[simp]
theorem dfinsupp.equiv_fun_on_fintype_apply {ι : Type u} {β : ι Type v} [Π (i : ι), has_zero (β i)] [fintype ι] (x : Π₀ (i : ι), β i) (i : ι) :
@[simp]
theorem dfinsupp.equiv_fun_on_fintype_symm_coe {ι : Type u} {β : ι Type v} [Π (i : ι), has_zero (β i)] [fintype ι] (f : Π₀ (i : ι), β i) :
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
theorem dfinsupp.single_eq_pi_single {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i : ι} {b : β i} :
b) = b
@[simp]
theorem dfinsupp.single_apply {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i i' : ι} {b : β i} :
b) i' = dite (i = i') (λ (h : i = i'), h.rec_on b) (λ (h : ¬i = i'), 0)
@[simp]
theorem dfinsupp.single_zero {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] (i : ι) :
= 0
@[simp]
theorem dfinsupp.single_eq_same {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i : ι} {b : β i} :
b) i = b
theorem dfinsupp.single_eq_of_ne {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i i' : ι} {b : β i} (h : i i') :
b) i' = 0
theorem dfinsupp.single_injective {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i : ι} :
theorem dfinsupp.single_eq_single_iff {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] (i j : ι) (xi : β i) (xj : β j) :
xi = xj i = j xi == xj xi = 0 xj = 0

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

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 : ι), (b i))

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

@[simp]
theorem dfinsupp.single_eq_zero {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i : ι} {xi : β i} :
xi = 0 xi = 0
theorem dfinsupp.filter_single {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] (p : ι Prop) (i : ι) (x : β i) :
x) = ite (p i) x) 0
@[simp]
theorem dfinsupp.filter_single_pos {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {p : ι Prop} (i : ι) (x : β i) (h : p i) :
x) =
@[simp]
theorem dfinsupp.filter_single_neg {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {p : ι Prop} (i : ι) (x : β i) (h : ¬p i) :
x) = 0
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⟩) :
xi = xj

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

@[simp]
theorem dfinsupp.equiv_fun_on_fintype_single {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [fintype ι] (i : ι) (m : β i) :
@[simp]
theorem dfinsupp.equiv_fun_on_fintype_symm_single {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [fintype ι] (i : ι) (m : β i) :
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
@[simp]
theorem dfinsupp.erase_apply {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i j : ι} {f : Π₀ (i : ι), β i} :
f) j = ite (j = i) 0 (f j)
@[simp]
theorem dfinsupp.erase_same {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i : ι} {f : Π₀ (i : ι), β i} :
f) i = 0
theorem dfinsupp.erase_ne {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i i' : ι} {f : Π₀ (i : ι), β i} (h : i' i) :
f) i' = f i'
theorem dfinsupp.piecewise_single_erase {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] (x : Π₀ (i : ι), β i) (i : ι) :
(x i)).piecewise x) {i} = x
theorem dfinsupp.erase_eq_sub_single {ι : Type u} [dec : decidable_eq ι] {β : ι Type u_1} [Π (i : ι), add_group (β i)] (f : Π₀ (i : ι), β i) (i : ι) :
= f - (f i)
@[simp]
theorem dfinsupp.erase_zero {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] (i : ι) :
= 0
@[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 =
@[simp]
theorem dfinsupp.filter_ne_eq_erase' {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] (f : Π₀ (i : ι), β i) (i : ι) :
f =
theorem dfinsupp.erase_single {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] (j i : ι) (x : β i) :
x) = ite (i = j) 0 x)
@[simp]
theorem dfinsupp.erase_single_same {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] (i : ι) (x : β i) :
x) = 0
@[simp]
theorem dfinsupp.erase_single_ne {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {i j : ι} (x : β i) (h : i j) :
x) =
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
@[simp]
theorem dfinsupp.coe_update {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] (i : ι) (f : Π₀ (i : ι), β i) (b : β i) :
f b) = b
@[simp]
theorem dfinsupp.update_self {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] (i : ι) (f : Π₀ (i : ι), β i) :
(f i) = f
@[simp]
theorem dfinsupp.update_eq_erase {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] (i : ι) (f : Π₀ (i : ι), β i) :
0 =
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) :
b = +
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) :
b = +
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) :
b = f - (f i) +
@[simp]
theorem dfinsupp.single_add {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] (i : ι) (b₁ b₂ : β i) :
(b₁ + b₂) = b₁ + b₂
@[simp]
theorem dfinsupp.erase_add {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] (i : ι) (f₁ f₂ : Π₀ (i : ι), β i) :
(f₁ + f₂) = f₁ + f₂
@[simp]
theorem dfinsupp.single_add_hom_apply {ι : Type u} (β : ι Type v) [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] (i : ι) (b : β i) :
b =
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
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
@[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) :
x =
@[simp]
theorem dfinsupp.single_neg {ι : Type u} [dec : decidable_eq ι] {β : ι Type v} [Π (i : ι), add_group (β i)] (i : ι) (x : β i) :
(-x) = -
@[simp]
theorem dfinsupp.single_sub {ι : Type u} [dec : decidable_eq ι] {β : ι Type v} [Π (i : ι), add_group (β i)] (i : ι) (x y : β i) :
(x - y) = -
@[simp]
theorem dfinsupp.erase_neg {ι : Type u} [dec : decidable_eq ι] {β : ι Type v} [Π (i : ι), add_group (β i)] (i : ι) (f : Π₀ (i : ι), β i) :
(-f) = -
@[simp]
theorem dfinsupp.erase_sub {ι : Type u} [dec : decidable_eq ι] {β : ι Type v} [Π (i : ι), add_group (β i)] (i : ι) (f g : Π₀ (i : ι), β i) :
(f - g) = -
theorem dfinsupp.single_add_erase {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] (i : ι) (f : Π₀ (i : ι), β i) :
(f i) + = f
theorem dfinsupp.erase_add_single {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] (i : ι) (f : Π₀ (i : ι), β i) :
+ (f i) = f
@[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 b + f)) :
p f
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 + b)) :
p f
@[simp]
theorem dfinsupp.add_closure_Union_range_single {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] :
theorem dfinsupp.add_hom_ext {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] {γ : Type w} ⦃f g : (Π₀ (i : ι), β i) →+ γ⦄ (H : (i : ι) (y : β i), f y) = g y)) :
f = g

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

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

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

@[simp]
theorem dfinsupp.mk_add {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), add_zero_class (β i)] {s : finset ι} {x y : Π (i : s), β i} :
(x + y) = x + y
@[simp]
theorem dfinsupp.mk_zero {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] {s : finset ι} :
0 = 0
@[simp]
theorem dfinsupp.mk_neg {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), add_group (β i)] {s : finset ι} {x : Π (i : s), β i.val} :
(-x) = - x
@[simp]
theorem dfinsupp.mk_sub {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), add_group (β i)] {s : finset ι} {x y : Π (i : s), β i.val} :
(x - y) = x - y
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
@[simp]
theorem dfinsupp.mk_smul {ι : Type u} {γ : Type w} {β : ι Type v} [dec : decidable_eq ι] [monoid γ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), (β i)] {s : finset ι} (c : γ) (x : Π (i : s), β i) :
(c x) = c x
@[simp]
theorem dfinsupp.single_smul {ι : Type u} {γ : Type w} {β : ι Type v} [dec : decidable_eq ι] [monoid γ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), (β i)] {i : ι} (c : γ) (x : β i) :
(c x) = c
def dfinsupp.support {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] (f : Π₀ (i : ι), β i) :

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

Equations
@[simp]
theorem dfinsupp.support_mk_subset {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {s : finset ι} {x : Π (i : s), β i.val} :
x).support s
@[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} :
@[simp]
theorem dfinsupp.mem_support_to_fun {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] (f : Π₀ (i : ι), β i) (i : ι) :
i f.support f i 0
theorem dfinsupp.eq_mk_support {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] (f : Π₀ (i : ι), β i) :
f = (λ (i : (f.support)), f i)
@[simp]
theorem dfinsupp.support_zero {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] :
theorem dfinsupp.mem_support_iff {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {f : Π₀ (i : ι), β i} {i : ι} :
i f.support f i 0
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
@[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 = 0
@[protected, instance]
def dfinsupp.decidable_zero {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] :
Equations
theorem dfinsupp.support_subset_iff {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {s : set ι} {f : Π₀ (i : ι), β i} :
(f.support) s (i : ι), i s f i = 0
theorem dfinsupp.support_single_ne_zero {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {i : ι} {b : β i} (hb : b 0) :
b).support = {i}
theorem dfinsupp.support_single_subset {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {i : ι} {b : β i} :
b).support {i}
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} :
g = (λ (i : (g.support)), f i.val (g i.val))
@[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} :
b) = (f i b)
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} :
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} :
g₁ g₂ = dfinsupp.mk (g₁.support g₂.support) (λ (i : (g₁.support g₂.support)), f i.val (g₁ i.val) (g₂ i.val))
theorem dfinsupp.support_zip_with {ι : Type u} {β : ι Type v} {β₁ : ι 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} :
hf g₁ g₂).support g₁.support g₂.support
theorem dfinsupp.erase_def {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] (i : ι) (f : Π₀ (i : ι), β i) :
= dfinsupp.mk (f.support.erase i) (λ (j : (f.support.erase i)), f j.val)
@[simp]
theorem dfinsupp.support_erase {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] (i : ι) (f : Π₀ (i : ι), β i) :
theorem dfinsupp.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) :
f b).support =
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)] :
f b).support = ite (b = 0) f).support f.support)
theorem dfinsupp.filter_def {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {p : ι Prop} (f : Π₀ (i : ι), β i) :
= (λ (i : f.support)), f i.val)
@[simp]
theorem dfinsupp.support_filter {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {p : ι Prop} (f : Π₀ (i : ι), β i) :
f).support =
theorem dfinsupp.subtype_domain_def {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {p : ι Prop} (f : Π₀ (i : ι), β i) :
= (λ (i : f.support)), f i)
@[simp]
theorem dfinsupp.support_subtype_domain {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {p : ι Prop} {f : Π₀ (i : ι), β i} :
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
@[simp]
theorem dfinsupp.support_neg {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), add_group (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {f : Π₀ (i : ι), β i} :
theorem dfinsupp.support_smul {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] {γ : Type w} [semiring γ] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), (β i)] [Π (i : ι) (x : β i), decidable (x 0)] (b : γ) (v : Π₀ (i : ι), β i) :
@[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
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
@[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 : κ) :
f) k = f (h k)
@[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) :
0 = 0
@[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) :
(f + g) = f + g
@[simp]
theorem dfinsupp.comap_domain_smul {ι : Type u} {γ : Type w} {β : ι Type v} [dec : decidable_eq ι] {κ : Type u_1} [monoid γ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), (β i)] (h : κ ι) (hh : function.injective h) (r : γ) (f : Π₀ (i : ι), β i) :
(r f) = r f
@[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.single (h k) x) =
def dfinsupp.comap_domain' {ι : Type u} {β : ι Type v} {κ : Type u_1} [Π (i : ι), has_zero (β i)] (h : κ ι) {h' : ι κ} (hh' : h) (f : Π₀ (i : ι), β i) :
Π₀ (k : κ), β (h k)

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

Equations
@[simp]
theorem dfinsupp.comap_domain'_apply {ι : Type u} {β : ι Type v} {κ : Type u_1} [Π (i : ι), has_zero (β i)] (h : κ ι) {h' : ι κ} (hh' : h) (f : Π₀ (i : ι), β i) (k : κ) :
hh' f) k = f (h k)
@[simp]
theorem dfinsupp.comap_domain'_zero {ι : Type u} {β : ι Type v} {κ : Type u_1} [Π (i : ι), has_zero (β i)] (h : κ ι) {h' : ι κ} (hh' : h) :
0 = 0
@[simp]
theorem dfinsupp.comap_domain'_add {ι : Type u} {β : ι Type v} {κ : Type u_1} [Π (i : ι), add_zero_class (β i)] (h : κ ι) {h' : ι κ} (hh' : h) (f g : Π₀ (i : ι), β i) :
(f + g) = f + g
@[simp]
theorem dfinsupp.comap_domain'_smul {ι : Type u} {γ : Type w} {β : ι Type v} {κ : Type u_1} [monoid γ] [Π (i : ι), add_monoid (β i)] [Π (i : ι), (β i)] (h : κ ι) {h' : ι κ} (hh' : h) (r : γ) (f : Π₀ (i : ι), β i) :
(r f) = r f
@[simp]
theorem dfinsupp.comap_domain'_single {ι : Type u} {β : ι Type v} {κ : Type u_1} [decidable_eq ι] [decidable_eq κ] [Π (i : ι), has_zero (β i)] (h : κ ι) {h' : ι κ} (hh' : h) (k : κ) (x : β (h k)) :
(dfinsupp.single (h k) x) =
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
@[simp]
theorem dfinsupp.equiv_congr_left_apply {ι : Type u} {β : ι Type v} {κ : Type u_1} [Π (i : ι), has_zero (β i)] (h : ι κ) (f : Π₀ (i : ι), (λ (i : ι), β i) i) :
= f
@[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
@[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
@[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
@[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), (δ i j)] :
(Π₀ (i : ι) (j : α i), δ i j)
Equations
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
@[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⟩
@[simp]
theorem dfinsupp.sigma_curry_zero {ι : Type u} {α : ι Type u_2} {δ : Π (i : ι), α i Type v} [Π (i : ι) (j : α i), has_zero (δ i j)] :
@[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 =
@[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), (δ i j)] (r : γ) (f : Π₀ (i : Σ (i : ι), α i), δ i.fst i.snd) :
@[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) :
x).sigma_curry = x)
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
@[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
@[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)] :
@[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) :
@[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), (δ i j)] (r : γ) (f : Π₀ (i : ι) (j : α i), δ i j) :
@[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) :
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
def dfinsupp.extend_with {ι : Type u} {α : 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
@[simp]
theorem dfinsupp.extend_with_none {ι : Type u} {α : Type v} [Π (i : option ι), has_zero (α i)] (f : Π₀ (i : ι), α (option.some i)) (a : α option.none) :
@[simp]
theorem dfinsupp.extend_with_some {ι : Type u} {α : Type v} [Π (i : option ι), has_zero (α i)] (f : Π₀ (i : ι), α (option.some i)) (a : α option.none) (i : ι) :
f) (option.some i) = f i
@[simp]
theorem dfinsupp.extend_with_single_zero {ι : Type u} {α : Type v} [decidable_eq ι] [Π (i : option ι), has_zero (α i)] (i : ι) (x : α (option.some i)) :
=
@[simp]
theorem dfinsupp.extend_with_zero {ι : Type u} {α : Type v} [decidable_eq ι] [Π (i : option ι), has_zero (α i)] (x : α option.none) :
@[simp]
theorem dfinsupp.equiv_prod_dfinsupp_symm_apply {ι : Type u} [dec : decidable_eq ι] {α : Type v} [Π (i : option ι), has_zero (α i)] (f : × Π₀ (i : ι), α (option.some i)) :
noncomputable def dfinsupp.equiv_prod_dfinsupp {ι : Type u} [dec : decidable_eq ι] {α : Type v} [Π (i : option ι), has_zero (α i)] :
(Π₀ (i : option ι), α i) × Π₀ (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
@[simp]
theorem dfinsupp.equiv_prod_dfinsupp_apply {ι : Type u} [dec : decidable_eq ι] {α : Type v} [Π (i : option ι), has_zero (α i)] (f : Π₀ (i : option ι), α i) :
theorem dfinsupp.equiv_prod_dfinsupp_add {ι : Type u} [dec : decidable_eq ι] {α : Type v} [Π (i : option ι), add_zero_class (α i)] (f g : Π₀ (i : option ι), α i) :
theorem dfinsupp.equiv_prod_dfinsupp_smul {ι : Type u} {γ : Type w} [dec : decidable_eq ι] {α : Type v} [monoid γ] [Π (i : option ι), add_monoid (α i)] [Π (i : option ι), (α i)] (r : γ) (f : Π₀ (i : option ι), α i) :
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
def dfinsupp.sum {ι : Type u} {γ : Type w} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i γ) :
γ

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

Equations
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)] {f : Π (i : ι), β₁ i β₂ i} {hf : (i : ι), f i 0 = 0} {g : Π₀ (i : ι), β₁ i} {h : Π (i : ι), β₂ i γ} (h0 : (i : ι), h i 0 = 0) :
hf g).sum h = g.sum (λ (i : ι) (b : β₁ i), h i (f i b))
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) :
hf g).prod h = g.prod (λ (i : ι) (b : β₁ i), h i (f i b))
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
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)] {h : Π (i : ι), β i γ} :
0.sum h = 0
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) :
b).prod h = h i b
theorem dfinsupp.sum_single_index {ι : Type u} {γ : Type w} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {i : ι} {b : β i} {h : Π (i : ι), β i γ} (h_zero : h i 0 = 0) :
b).sum h = h i b
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))
theorem dfinsupp.sum_neg_index {ι : Type u} {γ : Type w} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), add_group (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {g : Π₀ (i : ι), β i} {h : Π (i : ι), β i γ} (h0 : (i : ι), h i 0 = 0) :
(-g).sum h = g.sum (λ (i : ι) (b : β i), h i (-b))
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)] (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₂))
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₂))
@[simp]
theorem dfinsupp.sum_apply {ι : Type u} {β : ι Type v} {ι₁ : Type u₁} [decidable_eq ι₁] {β₁ : ι₁ Type v₁} [Π (i₁ : ι₁), has_zero (β₁ i₁)] [Π (i : ι₁) (x : β₁ i), decidable (x 0)] [Π (i : ι), add_comm_monoid (β i)] {f : Π₀ (i₁ : ι₁), β₁ i₁} {g : Π (i₁ : ι₁), β₁ i₁ (Π₀ (i : ι), β i)} {i₂ : ι} :
(f.sum g) i₂ = f.sum (λ (i₁ : ι₁) (b : β₁ i₁), (g i₁ b) i₂)
theorem dfinsupp.support_sum {ι : Type u} {β : ι Type v} [dec : decidable_eq ι] {ι₁ : Type u₁} [decidable_eq ι₁] {β₁ : ι₁ Type v₁} [Π (i₁ : ι₁), has_zero (β₁ i₁)] [Π (i : ι₁) (x : β₁ i), decidable (x 0)] [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {f : Π₀ (i₁ : ι₁), β₁ i₁} {g : Π (i₁ : ι₁), β₁ i₁ (Π₀ (i : ι), β i)} :
(f.sum g).support f.support.bUnion (λ (i : ι₁), (g i (f i)).support)
@[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
@[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)] {f : Π₀ (i : ι), β i} :
f.sum (λ (i : ι) (b : β i), 0) = 0
@[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)] {f : Π₀ (i : ι), β i} {h₁ h₂ : Π (i : ι), β i γ} :
f.sum (λ (i : ι) (b : β i), h₁ i b + h₂ i b) = f.sum h₁ + f.sum h₂
@[simp]
theorem dfinsupp.prod_mul {ι : Type u} {γ : Type 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₂
@[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)] {f : Π₀ (i : ι), β i} {h : Π (i : ι), β i γ} :
f.sum (λ (i : ι) (b : β i), -h i b) = -f.sum h
@[simp]
theorem dfinsupp.prod_inv {ι : Type u} {γ : Type 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)⁻¹
theorem dfinsupp.sum_eq_zero {ι : Type u} {γ : Type w} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {f : Π₀ (i : ι), β i} {h : Π (i : ι), β i γ} (hyp : (i : ι), h i (f i) = 0) :
f.sum h = 0
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
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)] [ γ] {f : Π₀ (i : ι), β i} {h : Π (i : ι), β i γ} {c : α} :
c f.sum h = f.sum (λ (a : ι) (b : β a), c h a b)
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)] {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
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
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} [ γ] [ γ] (s : S) (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i γ) (h : (c : ι), f c 0 g c (f c) s) :
f.prod g s
theorem dfinsupp_sum_mem {ι : Type u} {γ : Type w} {β : ι Type v} [dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {S : Type u_1} [