# Dependent functions with finite support #

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 (fun 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 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.sumAddHom 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 the Add instance 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 : ι) → 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 an implementation detail that aids computability; see the implementation notes in this file for more information.

• mk' :: (
• toFun : (i : ι) → β i

The underlying function of a dependent function with finite support (aka DFinsupp).

• support' : Trunc { s : // ∀ (i : ι), i s self.toFun i = 0 }

The support of a dependent function with finite support (aka DFinsupp).

• )
Instances For

Π₀ i, β i denotes the type of dependent functions with finite support DFinsupp β.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Pretty printer defined by notation3 command.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance DFinsupp.instDFunLike {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] :
DFunLike (Π₀ (i : ι), β i) ι β
Equations
• DFinsupp.instDFunLike = { coe := fun (f : Π₀ (i : ι), β i) => f.toFun, coe_injective' := }
instance DFinsupp.instCoeFunForall {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] :
CoeFun (Π₀ (i : ι), β i) fun (x : Π₀ (i : ι), β i) => (i : ι) → β i

Helper instance for when there are too many metavariables to apply DFunLike.coeFunForall directly.

Equations
• DFinsupp.instCoeFunForall = inferInstance
@[simp]
theorem DFinsupp.toFun_eq_coe {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] (f : Π₀ (i : ι), β i) :
f.toFun = f
theorem DFinsupp.ext_iff {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] {f : Π₀ (i : ι), β i} {g : Π₀ (i : ι), β i} :
f = g ∀ (i : ι), f i = g i
theorem DFinsupp.ext {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] {f : Π₀ (i : ι), β i} {g : Π₀ (i : ι), β i} (h : ∀ (i : ι), f i = g i) :
f = g
theorem DFinsupp.ne_iff {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] {f : Π₀ (i : ι), β i} {g : Π₀ (i : ι), β i} :
f g ∃ (i : ι), f i g i
instance DFinsupp.instZero {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] :
Zero (Π₀ (i : ι), β i)
Equations
• DFinsupp.instZero = { zero := { toFun := 0, support' := Trunc.mk , } }
instance DFinsupp.instInhabited {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] :
Inhabited (Π₀ (i : ι), β i)
Equations
• DFinsupp.instInhabited = { default := 0 }
@[simp]
theorem DFinsupp.coe_mk' {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] (f : (i : ι) → β i) (s : Trunc { s : // ∀ (i : ι), i s f i = 0 }) :
{ toFun := f, support' := s } = f
@[simp]
theorem DFinsupp.coe_zero {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] :
0 = 0
theorem DFinsupp.zero_apply {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] (i : ι) :
0 i = 0
def DFinsupp.mapRange {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → Zero (β₁ i)] [(i : ι) → 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 mapRange 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.mapRange.addMonoidHom
• DFinsupp.mapRange.addEquiv
• dfinsupp.mapRange.linearMap
• dfinsupp.mapRange.linearEquiv
Equations
• = { toFun := fun (i : ι) => f i (x i), support' := Trunc.map (fun (s : { s : // ∀ (i : ι), i s x.toFun i = 0 }) => s, ) x.support' }
Instances For
@[simp]
theorem DFinsupp.mapRange_apply {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → Zero (β₁ i)] [(i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ iβ₂ i) (hf : ∀ (i : ι), f i 0 = 0) (g : Π₀ (i : ι), β₁ i) (i : ι) :
(DFinsupp.mapRange f hf g) i = f i (g i)
@[simp]
theorem DFinsupp.mapRange_id {ι : Type u} {β₁ : ιType v₁} [(i : ι) → Zero (β₁ i)] (h : optParam (∀ (i : ι), id 0 = 0) ) (g : Π₀ (i : ι), β₁ i) :
DFinsupp.mapRange (fun (i : ι) => id) h g = g
theorem DFinsupp.mapRange_comp {ι : Type u} {β : ιType v} {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → Zero (β i)] [(i : ι) → Zero (β₁ i)] [(i : ι) → 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.mapRange (fun (i : ι) => f i f₂ i) h g = DFinsupp.mapRange f hf (DFinsupp.mapRange f₂ hf₂ g)
@[simp]
theorem DFinsupp.mapRange_zero {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → Zero (β₁ i)] [(i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ iβ₂ i) (hf : ∀ (i : ι), f i 0 = 0) :
= 0
def DFinsupp.zipWith {ι : Type u} {β : ιType v} {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → Zero (β i)] [(i : ι) → Zero (β₁ i)] [(i : ι) → 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 zipWith f hf is a binary operation Π₀ i, β₁ i → Π₀ i, β₂ i → Π₀ i, β i.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem DFinsupp.zipWith_apply {ι : Type u} {β : ιType v} {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → Zero (β i)] [(i : ι) → Zero (β₁ i)] [(i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ iβ₂ iβ i) (hf : ∀ (i : ι), f i 0 0 = 0) (g₁ : Π₀ (i : ι), β₁ i) (g₂ : Π₀ (i : ι), β₂ i) (i : ι) :
(DFinsupp.zipWith f hf g₁ g₂) i = f i (g₁ i) (g₂ i)
def DFinsupp.piecewise {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] (x : Π₀ (i : ι), β i) (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
Instances For
theorem DFinsupp.piecewise_apply {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] (x : Π₀ (i : ι), β i) (y : Π₀ (i : ι), β i) (s : Set ι) [(i : ι) → Decidable (i s)] (i : ι) :
(x.piecewise y s) i = if i s then x i else y i
@[simp]
theorem DFinsupp.coe_piecewise {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] (x : Π₀ (i : ι), β i) (y : Π₀ (i : ι), β i) (s : Set ι) [(i : ι) → Decidable (i s)] :
(x.piecewise y s) = s.piecewise x y
instance DFinsupp.instAdd {ι : Type u} {β : ιType v} [(i : ι) → AddZeroClass (β i)] :
Add (Π₀ (i : ι), β i)
Equations
• DFinsupp.instAdd = { add := DFinsupp.zipWith (fun (x : ι) (x_1 x_2 : β x) => x_1 + x_2) }
theorem DFinsupp.add_apply {ι : Type u} {β : ιType v} [(i : ι) → AddZeroClass (β i)] (g₁ : Π₀ (i : ι), β i) (g₂ : Π₀ (i : ι), β i) (i : ι) :
(g₁ + g₂) i = g₁ i + g₂ i
@[simp]
theorem DFinsupp.coe_add {ι : Type u} {β : ιType v} [(i : ι) → AddZeroClass (β i)] (g₁ : Π₀ (i : ι), β i) (g₂ : Π₀ (i : ι), β i) :
(g₁ + g₂) = g₁ + g₂
instance DFinsupp.addZeroClass {ι : Type u} {β : ιType v} [(i : ι) → AddZeroClass (β i)] :
AddZeroClass (Π₀ (i : ι), β i)
Equations
instance DFinsupp.instIsLeftCancelAdd {ι : Type u} {β : ιType v} [(i : ι) → AddZeroClass (β i)] [∀ (i : ι), IsLeftCancelAdd (β i)] :
IsLeftCancelAdd (Π₀ (i : ι), β i)
Equations
• =
instance DFinsupp.instIsRightCancelAdd {ι : Type u} {β : ιType v} [(i : ι) → AddZeroClass (β i)] [∀ (i : ι), IsRightCancelAdd (β i)] :
IsRightCancelAdd (Π₀ (i : ι), β i)
Equations
• =
instance DFinsupp.instIsCancelAdd {ι : Type u} {β : ιType v} [(i : ι) → AddZeroClass (β i)] [∀ (i : ι), IsCancelAdd (β i)] :
IsCancelAdd (Π₀ (i : ι), β i)
Equations
• =
instance DFinsupp.hasNatScalar {ι : Type u} {β : ιType v} [(i : ι) → AddMonoid (β i)] :
SMul (Π₀ (i : ι), β i)

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

Equations
• DFinsupp.hasNatScalar = { smul := fun (c : ) (v : Π₀ (i : ι), β i) => DFinsupp.mapRange (fun (x : ι) (x_1 : β x) => c x_1) v }
theorem DFinsupp.nsmul_apply {ι : Type u} {β : ιType v} [(i : ι) → AddMonoid (β i)] (b : ) (v : Π₀ (i : ι), β i) (i : ι) :
(b v) i = b v i
@[simp]
theorem DFinsupp.coe_nsmul {ι : Type u} {β : ιType v} [(i : ι) → AddMonoid (β i)] (b : ) (v : Π₀ (i : ι), β i) :
(b v) = b v
instance DFinsupp.instAddMonoid {ι : Type u} {β : ιType v} [(i : ι) → AddMonoid (β i)] :
AddMonoid (Π₀ (i : ι), β i)
Equations
def DFinsupp.coeFnAddMonoidHom {ι : Type u} {β : ιType v} [(i : ι) → AddZeroClass (β i)] :
(Π₀ (i : ι), β i) →+ (i : ι) → β i

Coercion from a DFinsupp to a pi type is an AddMonoidHom.

Equations
• DFinsupp.coeFnAddMonoidHom = { toFun := DFunLike.coe, map_zero' := , map_add' := }
Instances For
def DFinsupp.evalAddMonoidHom {ι : Type u} {β : ιType v} [(i : ι) → AddZeroClass (β i)] (i : ι) :
(Π₀ (i : ι), β i) →+ β i

Evaluation at a point is an AddMonoidHom. This is the finitely-supported version of Pi.evalAddMonoidHom.

Equations
• = .comp DFinsupp.coeFnAddMonoidHom
Instances For
instance DFinsupp.addCommMonoid {ι : Type u} {β : ιType v} [(i : ι) → AddCommMonoid (β i)] :
AddCommMonoid (Π₀ (i : ι), β i)
Equations
@[simp]
theorem DFinsupp.coe_finset_sum {ι : Type u} {β : ιType v} {α : Type u_1} [(i : ι) → AddCommMonoid (β i)] (s : ) (g : αΠ₀ (i : ι), β i) :
(∑ as, g a) = as, (g a)
@[simp]
theorem DFinsupp.finset_sum_apply {ι : Type u} {β : ιType v} {α : Type u_1} [(i : ι) → AddCommMonoid (β i)] (s : ) (g : αΠ₀ (i : ι), β i) (i : ι) :
(∑ as, g a) i = as, (g a) i
instance DFinsupp.instNeg {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] :
Neg (Π₀ (i : ι), β i)
Equations
• DFinsupp.instNeg = { neg := fun (f : Π₀ (i : ι), β i) => DFinsupp.mapRange (fun (x : ι) => Neg.neg) f }
theorem DFinsupp.neg_apply {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] (g : Π₀ (i : ι), β i) (i : ι) :
(-g) i = -g i
@[simp]
theorem DFinsupp.coe_neg {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] (g : Π₀ (i : ι), β i) :
(-g) = -g
instance DFinsupp.instSub {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] :
Sub (Π₀ (i : ι), β i)
Equations
theorem DFinsupp.sub_apply {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] (g₁ : Π₀ (i : ι), β i) (g₂ : Π₀ (i : ι), β i) (i : ι) :
(g₁ - g₂) i = g₁ i - g₂ i
@[simp]
theorem DFinsupp.coe_sub {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] (g₁ : Π₀ (i : ι), β i) (g₂ : Π₀ (i : ι), β i) :
(g₁ - g₂) = g₁ - g₂
instance DFinsupp.hasIntScalar {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] :
SMul (Π₀ (i : ι), β i)

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

Equations
• DFinsupp.hasIntScalar = { smul := fun (c : ) (v : Π₀ (i : ι), β i) => DFinsupp.mapRange (fun (x : ι) (x_1 : β x) => c x_1) v }
theorem DFinsupp.zsmul_apply {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] (b : ) (v : Π₀ (i : ι), β i) (i : ι) :
(b v) i = b v i
@[simp]
theorem DFinsupp.coe_zsmul {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] (b : ) (v : Π₀ (i : ι), β i) :
(b v) = b v
instance DFinsupp.instAddGroup {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] :
AddGroup (Π₀ (i : ι), β i)
Equations
instance DFinsupp.addCommGroup {ι : Type u} {β : ιType v} [(i : ι) → AddCommGroup (β i)] :
AddCommGroup (Π₀ (i : ι), β i)
Equations
instance DFinsupp.instSMulOfDistribMulAction {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] :
SMul γ (Π₀ (i : ι), β i)

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

Equations
• DFinsupp.instSMulOfDistribMulAction = { smul := fun (c : γ) (v : Π₀ (i : ι), β i) => DFinsupp.mapRange (fun (x : ι) (x_1 : β x) => c x_1) v }
theorem DFinsupp.smul_apply {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] (b : γ) (v : Π₀ (i : ι), β i) (i : ι) :
(b v) i = b v i
@[simp]
theorem DFinsupp.coe_smul {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] (b : γ) (v : Π₀ (i : ι), β i) :
(b v) = b v
instance DFinsupp.smulCommClass {ι : Type u} {γ : Type w} {β : ιType v} {δ : Type u_1} [] [] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] [(i : ι) → DistribMulAction δ (β i)] [∀ (i : ι), SMulCommClass γ δ (β i)] :
SMulCommClass γ δ (Π₀ (i : ι), β i)
Equations
• =
instance DFinsupp.isScalarTower {ι : Type u} {γ : Type w} {β : ιType v} {δ : Type u_1} [] [] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] [(i : ι) → DistribMulAction δ (β i)] [SMul γ δ] [∀ (i : ι), IsScalarTower γ δ (β i)] :
IsScalarTower γ δ (Π₀ (i : ι), β i)
Equations
• =
instance DFinsupp.isCentralScalar {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] [(i : ι) → DistribMulAction γᵐᵒᵖ (β i)] [∀ (i : ι), IsCentralScalar γ (β i)] :
IsCentralScalar γ (Π₀ (i : ι), β i)
Equations
• =
instance DFinsupp.distribMulAction {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] :
DistribMulAction γ (Π₀ (i : ι), β i)

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

Equations
instance DFinsupp.module {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module γ (β i)] :
Module γ (Π₀ (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 : ι) → 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
• = { toFun := fun (i : ι) => if p i then x i else 0, support' := Trunc.map (fun (xs : { s : // ∀ (i : ι), i s x.toFun i = 0 }) => xs, ) x.support' }
Instances For
@[simp]
theorem DFinsupp.filter_apply {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] (p : ιProp) [] (i : ι) (f : Π₀ (i : ι), β i) :
(DFinsupp.filter p f) i = if p i then f i else 0
theorem DFinsupp.filter_apply_pos {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] {p : ιProp} [] (f : Π₀ (i : ι), β i) {i : ι} (h : p i) :
(DFinsupp.filter p f) i = f i
theorem DFinsupp.filter_apply_neg {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] {p : ιProp} [] (f : Π₀ (i : ι), β i) {i : ι} (h : ¬p i) :
(DFinsupp.filter p f) i = 0
theorem DFinsupp.filter_pos_add_filter_neg {ι : Type u} {β : ιType v} [(i : ι) → AddZeroClass (β i)] (f : Π₀ (i : ι), β i) (p : ιProp) [] :
+ DFinsupp.filter (fun (i : ι) => ¬p i) f = f
@[simp]
theorem DFinsupp.filter_zero {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] (p : ιProp) [] :
= 0
@[simp]
theorem DFinsupp.filter_add {ι : Type u} {β : ιType v} [(i : ι) → AddZeroClass (β i)] (p : ιProp) [] (f : Π₀ (i : ι), β i) (g : Π₀ (i : ι), β i) :
DFinsupp.filter p (f + g) = +
@[simp]
theorem DFinsupp.filter_smul {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] (p : ιProp) [] (r : γ) (f : Π₀ (i : ι), β i) :
@[simp]
theorem DFinsupp.filterAddMonoidHom_apply {ι : Type u} (β : ιType v) [(i : ι) → AddZeroClass (β i)] (p : ιProp) [] (x : Π₀ (i : ι), β i) :
x =
def DFinsupp.filterAddMonoidHom {ι : Type u} (β : ιType v) [(i : ι) → AddZeroClass (β i)] (p : ιProp) [] :
(Π₀ (i : ι), β i) →+ Π₀ (i : ι), β i

DFinsupp.filter as an AddMonoidHom.

Equations
• = { toFun := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem DFinsupp.filterLinearMap_apply {ι : Type u} (γ : Type w) (β : ιType v) [] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module γ (β i)] (p : ιProp) [] (x : Π₀ (i : ι), β i) :
x =
def DFinsupp.filterLinearMap {ι : Type u} (γ : Type w) (β : ιType v) [] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module γ (β i)] (p : ιProp) [] :
(Π₀ (i : ι), β i) →ₗ[γ] Π₀ (i : ι), β i

DFinsupp.filter as a LinearMap.

Equations
• = { toFun := , map_add' := , map_smul' := }
Instances For
@[simp]
theorem DFinsupp.filter_neg {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] (p : ιProp) [] (f : Π₀ (i : ι), β i) :
@[simp]
theorem DFinsupp.filter_sub {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] (p : ιProp) [] (f : Π₀ (i : ι), β i) (g : Π₀ (i : ι), β i) :
DFinsupp.filter p (f - g) = -
def DFinsupp.subtypeDomain {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] (p : ιProp) [] (x : Π₀ (i : ι), β i) :
Π₀ (i : ), β i

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem DFinsupp.subtypeDomain_zero {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] {p : ιProp} [] :
@[simp]
theorem DFinsupp.subtypeDomain_apply {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] {p : ιProp} [] {i : } {v : Π₀ (i : ι), β i} :
i = v i
@[simp]
theorem DFinsupp.subtypeDomain_add {ι : Type u} {β : ιType v} [(i : ι) → AddZeroClass (β i)] {p : ιProp} [] (v : Π₀ (i : ι), β i) (v' : Π₀ (i : ι), β i) :
@[simp]
theorem DFinsupp.subtypeDomain_smul {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] {p : ιProp} [] (r : γ) (f : Π₀ (i : ι), β i) :
@[simp]
theorem DFinsupp.subtypeDomainAddMonoidHom_apply {ι : Type u} (β : ιType v) [(i : ι) → AddZeroClass (β i)] (p : ιProp) [] (x : Π₀ (i : ι), β i) :
def DFinsupp.subtypeDomainAddMonoidHom {ι : Type u} (β : ιType v) [(i : ι) → AddZeroClass (β i)] (p : ιProp) [] :
(Π₀ (i : ι), β i) →+ Π₀ (i : ), β i

subtypeDomain but as an AddMonoidHom.

Equations
• = { toFun := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem DFinsupp.subtypeDomainLinearMap_apply {ι : Type u} (γ : Type w) (β : ιType v) [] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module γ (β i)] (p : ιProp) [] (x : Π₀ (i : ι), β i) :
x =
def DFinsupp.subtypeDomainLinearMap {ι : Type u} (γ : Type w) (β : ιType v) [] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module γ (β i)] (p : ιProp) [] :
(Π₀ (i : ι), β i) →ₗ[γ] Π₀ (i : ), β i

DFinsupp.subtypeDomain as a LinearMap.

Equations
• = { toFun := , map_add' := , map_smul' := }
Instances For
@[simp]
theorem DFinsupp.subtypeDomain_neg {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] {p : ιProp} [] {v : Π₀ (i : ι), β i} :
@[simp]
theorem DFinsupp.subtypeDomain_sub {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] {p : ιProp} [] {v : Π₀ (i : ι), β i} {v' : Π₀ (i : ι), β i} :
theorem DFinsupp.finite_support {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] (f : Π₀ (i : ι), β i) :
{i : ι | f i 0}.Finite
def DFinsupp.mk {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] (s : ) (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
• = { toFun := fun (i : ι) => if H : i s then x i, H else 0, support' := Trunc.mk s.val, }
Instances For
@[simp]
theorem DFinsupp.mk_apply {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] {s : } {x : (i : s) → β i} {i : ι} :
(DFinsupp.mk s x) i = if H : i s then x i, H else 0
theorem DFinsupp.mk_of_mem {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] {s : } {x : (i : s) → β i} {i : ι} (hi : i s) :
(DFinsupp.mk s x) i = x i, hi
theorem DFinsupp.mk_of_not_mem {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] {s : } {x : (i : s) → β i} {i : ι} (hi : is) :
(DFinsupp.mk s x) i = 0
theorem DFinsupp.mk_injective {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] (s : ) :
instance DFinsupp.unique {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [∀ (i : ι), Subsingleton (β i)] :
Unique (Π₀ (i : ι), β i)
Equations
• DFinsupp.unique = .unique
instance DFinsupp.uniqueOfIsEmpty {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] :
Unique (Π₀ (i : ι), β i)
Equations
• DFinsupp.uniqueOfIsEmpty = .unique
@[simp]
theorem DFinsupp.equivFunOnFintype_apply {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] :
∀ (a : Π₀ (i : ι), β i) (a_1 : ι), DFinsupp.equivFunOnFintype a a_1 = a a_1
def DFinsupp.equivFunOnFintype {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] :
(Π₀ (i : ι), β i) ((i : ι) → β i)

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

Equations
• DFinsupp.equivFunOnFintype = { toFun := DFunLike.coe, invFun := fun (f : (i : ι) → β i) => { toFun := f, support' := Trunc.mk Finset.univ.val, }, left_inv := , right_inv := }
Instances For
@[simp]
theorem DFinsupp.equivFunOnFintype_symm_coe {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] (f : Π₀ (i : ι), β i) :
DFinsupp.equivFunOnFintype.symm f = f
def DFinsupp.single {ι : Type u} {β : ιType v} [(i : ι) → 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
• = { toFun := , support' := Trunc.mk {i}, }
Instances For
theorem DFinsupp.single_eq_pi_single {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] {i : ι} {b : β i} :
(DFinsupp.single i b) =
@[simp]
theorem DFinsupp.single_apply {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] {i : ι} {i' : ι} {b : β i} :
(DFinsupp.single i b) i' = if h : i = i' then Eq.recOn h b else 0
@[simp]
theorem DFinsupp.single_zero {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] (i : ι) :
= 0
theorem DFinsupp.single_eq_same {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] {i : ι} {b : β i} :
(DFinsupp.single i b) i = b
theorem DFinsupp.single_eq_of_ne {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] {i : ι} {i' : ι} {b : β i} (h : i i') :
(DFinsupp.single i b) i' = 0
theorem DFinsupp.single_injective {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] {i : ι} :
theorem DFinsupp.single_eq_single_iff {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] (i : ι) (j : ι) (xi : β i) (xj : β j) :
= i = j HEq 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} [(i : ι) → Zero (β i)] [] {b : (i : ι) → β i} (h : ∀ (i : ι), b i 0) :
Function.Injective fun (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

@[simp]
theorem DFinsupp.single_eq_zero {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] {i : ι} {xi : β i} :
= 0 xi = 0
theorem DFinsupp.filter_single {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] (p : ιProp) [] (i : ι) (x : β i) :
= if p i then else 0
@[simp]
theorem DFinsupp.filter_single_pos {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] {p : ιProp} [] (i : ι) (x : β i) (h : p i) :
=
@[simp]
theorem DFinsupp.filter_single_neg {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] {p : ιProp} [] (i : ι) (x : β i) (h : ¬p i) :
= 0
theorem DFinsupp.single_eq_of_sigma_eq {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] {i : ι} {j : ι} {xi : β i} {xj : β j} (h : i, xi = j, xj) :
=

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

@[simp]
theorem DFinsupp.equivFunOnFintype_single {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] [] (i : ι) (m : β i) :
DFinsupp.equivFunOnFintype (DFinsupp.single i m) =
@[simp]
theorem DFinsupp.equivFunOnFintype_symm_single {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] [] (i : ι) (m : β i) :
DFinsupp.equivFunOnFintype.symm (Pi.single i m) =
@[simp]
theorem DFinsupp.zipWith_single_single {ι : Type u} {β : ιType v} {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → Zero (β i)] [] [(i : ι) → Zero (β₁ i)] [(i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ iβ₂ iβ i) (hf : ∀ (i : ι), f i 0 0 = 0) {i : ι} (b₁ : β₁ i) (b₂ : β₂ i) :
DFinsupp.zipWith f hf (DFinsupp.single i b₁) (DFinsupp.single i b₂) = DFinsupp.single i (f i b₁ b₂)
def DFinsupp.erase {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] (i : ι) (x : Π₀ (i : ι), β i) :
Π₀ (i : ι), β i

Redefine f i to be 0.

Equations
• = { toFun := fun (j : ι) => if j = i then 0 else x.toFun j, support' := Trunc.map (fun (xs : { s : // ∀ (i : ι), i s x.toFun i = 0 }) => xs, ) x.support' }
Instances For
@[simp]
theorem DFinsupp.erase_apply {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] {i : ι} {j : ι} {f : Π₀ (i : ι), β i} :
(DFinsupp.erase i f) j = if j = i then 0 else f j
theorem DFinsupp.erase_same {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] {i : ι} {f : Π₀ (i : ι), β i} :
(DFinsupp.erase i f) i = 0
theorem DFinsupp.erase_ne {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] {i : ι} {i' : ι} {f : Π₀ (i : ι), β i} (h : i' i) :
(DFinsupp.erase i f) i' = f i'
theorem DFinsupp.piecewise_single_erase {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] (x : Π₀ (i : ι), β i) (i : ι) [(i' : ι) → Decidable (i' {i})] :
(DFinsupp.single i (x i)).piecewise (DFinsupp.erase i x) {i} = x
theorem DFinsupp.erase_eq_sub_single {ι : Type u} [] {β : ιType u_1} [(i : ι) → AddGroup (β i)] (f : Π₀ (i : ι), β i) (i : ι) :
= f - DFinsupp.single i (f i)
@[simp]
theorem DFinsupp.erase_zero {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] (i : ι) :
= 0
@[simp]
theorem DFinsupp.filter_ne_eq_erase {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] (f : Π₀ (i : ι), β i) (i : ι) :
DFinsupp.filter (fun (x : ι) => x i) f =
@[simp]
theorem DFinsupp.filter_ne_eq_erase' {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] (f : Π₀ (i : ι), β i) (i : ι) :
DFinsupp.filter (fun (x : ι) => i x) f =
theorem DFinsupp.erase_single {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] (j : ι) (i : ι) (x : β i) :
= if i = j then 0 else
@[simp]
theorem DFinsupp.erase_single_same {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] (i : ι) (x : β i) :
= 0
@[simp]
theorem DFinsupp.erase_single_ne {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] {i : ι} {j : ι} (x : β i) (h : i j) :
=
def DFinsupp.update {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] (f : Π₀ (i : ι), β 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
Instances For
@[simp]
theorem DFinsupp.coe_update {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] (f : Π₀ (i : ι), β i) (i : ι) (b : β i) :
(f.update i b) = Function.update (⇑f) i b
@[simp]
theorem DFinsupp.update_self {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] (f : Π₀ (i : ι), β i) (i : ι) :
f.update i (f i) = f
@[simp]
theorem DFinsupp.update_eq_erase {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [] (f : Π₀ (i : ι), β i) (i : ι) :
f.update i 0 =
theorem DFinsupp.update_eq_single_add_erase {ι : Type u} [] {β : ιType u_1} [(i : ι) → AddZeroClass (β i)] (f : Π₀ (i : ι), β i) (i : ι) (b : β i) :
f.update i b = +
theorem DFinsupp.update_eq_erase_add_single {ι : Type u} [] {β : ιType u_1} [(i : ι) → AddZeroClass (β i)] (f : Π₀ (i : ι), β i) (i : ι) (b : β i) :
f.update i b = +
theorem DFinsupp.update_eq_sub_add_single {ι : Type u} [] {β : ιType u_1} [(i : ι) → AddGroup (β i)] (f : Π₀ (i : ι), β i) (i : ι) (b : β i) :
f.update i b = f - DFinsupp.single i (f i) +
@[simp]
theorem DFinsupp.single_add {ι : Type u} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] (i : ι) (b₁ : β i) (b₂ : β i) :
DFinsupp.single i (b₁ + b₂) = +
@[simp]
theorem DFinsupp.erase_add {ι : Type u} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] (i : ι) (f₁ : Π₀ (i : ι), β i) (f₂ : Π₀ (i : ι), β i) :
DFinsupp.erase i (f₁ + f₂) = +
@[simp]
theorem DFinsupp.singleAddHom_apply {ι : Type u} (β : ιType v) [] [(i : ι) → AddZeroClass (β i)] (i : ι) (b : β i) :
b =
def DFinsupp.singleAddHom {ι : Type u} (β : ιType v) [] [(i : ι) → AddZeroClass (β i)] (i : ι) :
β i →+ Π₀ (i : ι), β i

DFinsupp.single as an AddMonoidHom.

Equations
• = { toFun := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem DFinsupp.eraseAddHom_apply {ι : Type u} (β : ιType v) [] [(i : ι) → AddZeroClass (β i)] (i : ι) (x : Π₀ (i : ι), β i) :
x =
def DFinsupp.eraseAddHom {ι : Type u} (β : ιType v) [] [(i : ι) → AddZeroClass (β i)] (i : ι) :
(Π₀ (i : ι), β i) →+ Π₀ (i : ι), β i

DFinsupp.erase as an AddMonoidHom.

Equations
• = { toFun := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem DFinsupp.single_neg {ι : Type u} [] {β : ιType v} [(i : ι) → AddGroup (β i)] (i : ι) (x : β i) :
@[simp]
theorem DFinsupp.single_sub {ι : Type u} [] {β : ιType v} [(i : ι) → AddGroup (β i)] (i : ι) (x : β i) (y : β i) :
DFinsupp.single i (x - y) = -
@[simp]
theorem DFinsupp.erase_neg {ι : Type u} [] {β : ιType v} [(i : ι) → AddGroup (β i)] (i : ι) (f : Π₀ (i : ι), β i) :
@[simp]
theorem DFinsupp.erase_sub {ι : Type u} [] {β : ιType v} [(i : ι) → AddGroup (β i)] (i : ι) (f : Π₀ (i : ι), β i) (g : Π₀ (i : ι), β i) :
DFinsupp.erase i (f - g) = -
theorem DFinsupp.single_add_erase {ι : Type u} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] (i : ι) (f : Π₀ (i : ι), β i) :
DFinsupp.single i (f i) + = f
theorem DFinsupp.erase_add_single {ι : Type u} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] (i : ι) (f : Π₀ (i : ι), β i) :
+ DFinsupp.single i (f i) = f
theorem DFinsupp.induction {ι : Type u} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] {p : (Π₀ (i : ι), β i)Prop} (f : Π₀ (i : ι), β i) (h0 : p 0) (ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0b 0p fp ( + f)) :
p f
theorem DFinsupp.induction₂ {ι : Type u} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] {p : (Π₀ (i : ι), β i)Prop} (f : Π₀ (i : ι), β i) (h0 : p 0) (ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0b 0p fp (f + )) :
p f
@[simp]
theorem DFinsupp.add_closure_iUnion_range_single {ι : Type u} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] :
AddSubmonoid.closure (⋃ (i : ι), ) =
theorem DFinsupp.addHom_ext {ι : Type u} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] {γ : Type w} [] ⦃f : (Π₀ (i : ι), β i) →+ γ ⦃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.

theorem DFinsupp.addHom_ext'_iff {ι : Type u} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] {γ : Type w} [] {f : (Π₀ (i : ι), β i) →+ γ} {g : (Π₀ (i : ι), β i) →+ γ} :
f = g ∀ (x : ι), f.comp = g.comp
theorem DFinsupp.addHom_ext' {ι : Type u} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] {γ : Type w} [] ⦃f : (Π₀ (i : ι), β i) →+ γ ⦃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.

See note [partially-applied ext lemmas].

@[simp]
theorem DFinsupp.mk_add {ι : Type u} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] {s : } {x : (i : s) → β i} {y : (i : s) → β i} :
DFinsupp.mk s (x + y) = +
@[simp]
theorem DFinsupp.mk_zero {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] {s : } :
= 0
@[simp]
theorem DFinsupp.mk_neg {ι : Type u} {β : ιType v} [] [(i : ι) → AddGroup (β i)] {s : } {x : (i : s) → β i} :
@[simp]
theorem DFinsupp.mk_sub {ι : Type u} {β : ιType v} [] [(i : ι) → AddGroup (β i)] {s : } {x : (i : s) → β i} {y : (i : s) → β i} :
DFinsupp.mk s (x - y) = -
def DFinsupp.mkAddGroupHom {ι : Type u} {β : ιType v} [] [(i : ι) → AddGroup (β i)] (s : ) :
((i : s) → β i) →+ Π₀ (i : ι), β i

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

Equations
• = { toFun := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem DFinsupp.mk_smul {ι : Type u} {γ : Type w} {β : ιType v} [] [] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] {s : } (c : γ) (x : (i : s) → β i) :
DFinsupp.mk s (c x) = c
@[simp]
theorem DFinsupp.single_smul {ι : Type u} {γ : Type w} {β : ιType v} [] [] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] {i : ι} (c : γ) (x : β i) :
def DFinsupp.support {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] (f : Π₀ (i : ι), β i) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem DFinsupp.support_mk_subset {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] {s : } {x : (i : s) → β i} :
(DFinsupp.mk s x).support s
@[simp]
theorem DFinsupp.support_mk'_subset {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] {f : (i : ι) → β i} {s : } {h : ∀ (i : ι), i s f i = 0} :
{ toFun := f, support' := Trunc.mk s, h }.support s.toFinset
@[simp]
theorem DFinsupp.mem_support_toFun {ι : Type u} {β : ιType v} [] [(i : ι) → 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} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] (f : Π₀ (i : ι), β i) :
f = DFinsupp.mk f.support fun (i : f.support) => f i
@[simp]
theorem DFinsupp.subtypeSupportEqEquiv_apply_coe {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] (s : ) :
∀ (x : { f : Π₀ (i : ι), β i // f.support = s }) (i : { x : ι // x s }), ( x i) = x i
@[simp]
theorem DFinsupp.subtypeSupportEqEquiv_symm_apply_coe {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] (s : ) (f : (i : { x : ι // x s }) → { x : β i // x 0 }) :
(.symm f) = DFinsupp.mk s fun (i : s) => (f i)
def DFinsupp.subtypeSupportEqEquiv {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] (s : ) :
{ f : Π₀ (i : ι), β i // f.support = s } ((i : { x : ι // x s }) → { x : β i // x 0 })

Equivalence between dependent functions with finite support s : Finset ι and functions ∀ i, {x : β i // x ≠ 0}.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem DFinsupp.sigmaFinsetFunEquiv_apply_fst {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] :
∀ (a : Π₀ (i : ι), β i), (DFinsupp.sigmaFinsetFunEquiv a).fst = a.support
@[simp]
theorem DFinsupp.sigmaFinsetFunEquiv_apply_snd_coe {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] :
∀ (a : Π₀ (i : ι), β i) (i : { x : ι // x ((Equiv.sigmaFiberEquiv DFinsupp.support).symm a).fst }), ((DFinsupp.sigmaFinsetFunEquiv a).snd i) = a i
def DFinsupp.sigmaFinsetFunEquiv {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] :
(Π₀ (i : ι), β i) (s : ) × ((i : { x : ι // x s }) → { x : β i // x 0 })

Equivalence between all dependent finitely supported functions f : Π₀ i, β i and type of pairs ⟨s : Finset ι, f : ∀ i : s, {x : β i // x ≠ 0}⟩.

Equations
Instances For
@[simp]
theorem DFinsupp.support_zero {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] :
theorem DFinsupp.mem_support_iff {ι : Type u} {β : ιType v} [] [(i : ι) → 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} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] {f : Π₀ (i : ι), β i} {i : ι} :
if.support f i = 0
@[simp]
theorem DFinsupp.support_eq_empty {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] {f : Π₀ (i : ι), β i} :
f.support = f = 0
instance DFinsupp.decidableZero {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x = 0)] (f : Π₀ (i : ι), β i) :
Decidable (f = 0)
Equations
• f.decidableZero = f.support'.recOnSubsingleton fun (s : { s : // ∀ (i : ι), i s f.toFun i = 0 }) => decidable_of_iff (∀ is, f i = 0)
theorem DFinsupp.support_subset_iff {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] {s : Set ι} {f : Π₀ (i : ι), β i} :
f.support s is, f i = 0
theorem DFinsupp.support_single_ne_zero {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] {i : ι} {b : β i} (hb : b 0) :
(DFinsupp.single i b).support = {i}
theorem DFinsupp.support_single_subset {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] {i : ι} {b : β i} :
(DFinsupp.single i b).support {i}
theorem DFinsupp.mapRange_def {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [] [(i : ι) → Zero (β₁ i)] [(i : ι) → Zero (β₂ i)] [(i : ι) → (x : β₁ i) → Decidable (x 0)] {f : (i : ι) → β₁ iβ₂ i} {hf : ∀ (i : ι), f i 0 = 0} {g : Π₀ (i : ι), β₁ i} :
= DFinsupp.mk g.support fun (i : g.support) => f (↑i) (g i)
@[simp]
theorem DFinsupp.mapRange_single {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [] [(i : ι) → Zero (β₁ i)] [(i : ι) → Zero (β₂ i)] {f : (i : ι) → β₁ iβ₂ i} {hf : ∀ (i : ι), f i 0 = 0} {i : ι} {b : β₁ i} :
theorem DFinsupp.support_mapRange {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [] [(i : ι) → Zero (β₁ i)] [(i : ι) → 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.mapRange f hf g).support g.support
theorem DFinsupp.zipWith_def {ι : Type u} {β : ιType v} {β₁ : ιType v₁} {β₂ : ιType v₂} [dec : ] [(i : ι) → Zero (β i)] [(i : ι) → Zero (β₁ i)] [(i : ι) → 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.zipWith f hf g₁ g₂ = DFinsupp.mk (g₁.support g₂.support) fun (i : (g₁.support g₂.support)) => f (↑i) (g₁ i) (g₂ i)
theorem DFinsupp.support_zipWith {ι : Type u} {β : ιType v} {β₁ : ιType v₁} {β₂ : ιType v₂} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [(i : ι) → Zero (β₁ i)] [(i : ι) → 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.zipWith f hf g₁ g₂).support g₁.support g₂.support
theorem DFinsupp.erase_def {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] (i : ι) (f : Π₀ (i : ι), β i) :
= DFinsupp.mk (f.support.erase i) fun (j : (f.support.erase i)) => f j
@[simp]
theorem DFinsupp.support_erase {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] (i : ι) (f : Π₀ (i : ι), β i) :
(DFinsupp.erase i f).support = f.support.erase i
theorem DFinsupp.support_update_ne_zero {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] (f : Π₀ (i : ι), β i) (i : ι) {b : β i} (h : b 0) :
(f.update i b).support = insert i f.support
theorem DFinsupp.support_update {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] (f : Π₀ (i : ι), β i) (i : ι) (b : β i) [Decidable (b = 0)] :
(f.update i b).support = if b = 0 then (DFinsupp.erase i f).support else insert i f.support
theorem DFinsupp.filter_def {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] {p : ιProp} [] (f : Π₀ (i : ι), β i) :
= DFinsupp.mk (Finset.filter p f.support) fun (i : (Finset.filter p f.support)) => f i
@[simp]
theorem DFinsupp.support_filter {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] {p : ιProp} [] (f : Π₀ (i : ι), β i) :
(DFinsupp.filter p f).support = Finset.filter p f.support
theorem DFinsupp.subtypeDomain_def {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] {p : ιProp} [] (f : Π₀ (i : ι), β i) :
= DFinsupp.mk (Finset.subtype p f.support) fun (i : (Finset.subtype p f.support)) => f i
@[simp]
theorem DFinsupp.support_subtypeDomain {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] {p : ιProp} [] {f : Π₀ (i : ι), β i} :
.support = Finset.subtype p f.support
theorem DFinsupp.support_add {ι : Type u} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] {g₁ : Π₀ (i : ι), β i} {g₂ : Π₀ (i : ι), β i} :
(g₁ + g₂).support g₁.support g₂.support
@[simp]
theorem DFinsupp.support_neg {ι : Type u} {β : ιType v} [] [(i : ι) → AddGroup (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] {f : Π₀ (i : ι), β i} :
(-f).support = f.support
theorem DFinsupp.support_smul {ι : Type u} {β : ιType v} [] {γ : Type w} [] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module γ (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] (b : γ) (v : Π₀ (i : ι), β i) :
(b v).support v.support
instance DFinsupp.instDecidableEq {ι : Type u} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] :
DecidableEq (Π₀ (i : ι), β i)
Equations
noncomputable def DFinsupp.comapDomain {ι : Type u} {β : ιType v} {κ : Type u_1} [(i : ι) → Zero (β i)] (h : κι) (hh : ) (f : Π₀ (i : ι), β i) :
Π₀ (k : κ), β (h k)

Reindexing (and possibly removing) terms of a dfinsupp.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem DFinsupp.comapDomain_apply {ι : Type u} {β : ιType v} {κ : Type u_1} [(i : ι) → Zero (β i)] (h : κι) (hh : ) (f : Π₀ (i : ι), β i) (k : κ) :
(DFinsupp.comapDomain h hh f) k = f (h k)
@[simp]
theorem DFinsupp.comapDomain_zero {ι : Type u} {β : ιType v} {κ : Type u_1} [(i : ι) → Zero (β i)] (h : κι) (hh : ) :
= 0
@[simp]
theorem DFinsupp.comapDomain_add {ι : Type u} {β : ιType v} {κ : Type u_1} [(i : ι) → AddZeroClass (β i)] (h : κι) (hh : ) (f : Π₀ (i : ι), β i) (g : Π₀ (i : ι), β i) :
@[simp]
theorem DFinsupp.comapDomain_smul {ι : Type u} {γ : Type w} {β : ιType v} {κ : Type u_1} [] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] (h : κι) (hh : ) (r : γ) (f : Π₀ (i : ι), β i) :
@[simp]
theorem DFinsupp.comapDomain_single {ι : Type u} {β : ιType v} {κ : Type u_1} [] [] [(i : ι) → Zero (β i)] (h : κι) (hh : ) (k : κ) (x : β (h k)) :
def DFinsupp.comapDomain' {ι : Type u} {β : ιType v} {κ : Type u_1} [(i : ι) → Zero (β i)] (h : κι) {h' : ικ} (hh' : ) (f : Π₀ (i : ι), β i) :
Π₀ (k : κ), β (h k)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem DFinsupp.comapDomain'_apply {ι : Type u} {β : ιType v} {κ : Type u_1} [(i : ι) → Zero (β i)] (h : κι) {h' : ικ} (hh' : ) (f : Π₀ (i : ι), β i) (k : κ) :
(DFinsupp.comapDomain' h hh' f) k = f (h k)
@[simp]
theorem DFinsupp.comapDomain'_zero {ι : Type u} {β : ιType v} {κ : Type u_1} [(i : ι) → Zero (β i)] (h : κι) {h' : ικ} (hh' : ) :
= 0
@[simp]
theorem DFinsupp.comapDomain'_add {ι : Type u} {β : ιType v} {κ : Type u_1} [(i : ι) → AddZeroClass (β i)] (h : κι) {h' : ικ} (hh' : ) (f : Π₀ (i : ι), β i) (g : Π₀ (i : ι), β i) :
DFinsupp.comapDomain' h hh' (f + g) = +
@[simp]
theorem DFinsupp.comapDomain'_smul {ι : Type u} {γ : Type w} {β : ιType v} {κ : Type u_1} [] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] (h : κι) {h' : ικ} (hh' : ) (r : γ) (f : Π₀ (i : ι), β i) :
@[simp]
theorem DFinsupp.comapDomain'_single {ι : Type u} {β : ιType v} {κ : Type u_1} [] [] [(i : ι) → Zero (β i)] (h : κι) {h' : ικ} (hh' : ) (k : κ) (x : β (h k)) :
@[simp]
theorem DFinsupp.equivCongrLeft_apply {ι : Type u} {β : ιType v} {κ : Type u_1} [(i : ι) → Zero (β i)] (h : ι κ) (f : Π₀ (i : ι), β i) :
= DFinsupp.comapDomain' h.symm f
def DFinsupp.equivCongrLeft {ι : Type u} {β : ιType v} {κ : Type u_1} [(i : ι) → Zero (β i)] (h : ι κ) :
(Π₀ (i : ι), β i) Π₀ (k : κ), β (h.symm k)

Reindexing terms of a dfinsupp.

This is the dfinsupp version of Equiv.piCongrLeft'.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance DFinsupp.hasAdd₂ {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [(i : ι) → (j : α i) → AddZeroClass (δ i j)] :
Add (Π₀ (i : ι) (j : α i), δ i j)
Equations
• DFinsupp.hasAdd₂ = inferInstance
instance DFinsupp.addZeroClass₂ {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [(i : ι) → (j : α i) → AddZeroClass (δ i j)] :
AddZeroClass (Π₀ (i : ι) (j : α i), δ i j)
Equations
• DFinsupp.addZeroClass₂ = inferInstance
instance DFinsupp.addMonoid₂ {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [(i : ι) → (j : α i) → AddMonoid (δ i j)] :
AddMonoid (Π₀ (i : ι) (j : α i), δ i j)
Equations
• DFinsupp.addMonoid₂ = inferInstance
instance DFinsupp.distribMulAction₂ {ι : Type u} {γ : Type w} {α : ιType u_2} {δ : (i : ι) → α iType v} [] [(i : ι) → (j : α i) → AddMonoid (δ i j)] [(i : ι) → (j : α i) → DistribMulAction γ (δ i j)] :
DistribMulAction γ (Π₀ (i : ι) (j : α i), δ i j)
Equations
• DFinsupp.distribMulAction₂ = DFinsupp.distribMulAction
def DFinsupp.sigmaCurry {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [] [(i : ι) → (j : α i) → Zero (δ i j)] (f : Π₀ (i : (x : ι) × α x), δ 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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem DFinsupp.sigmaCurry_apply {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [] [(i : ι) → (j : α i) → Zero (δ i j)] (f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd) (i : ι) (j : α i) :
(f.sigmaCurry i) j = f i, j
@[simp]
theorem DFinsupp.sigmaCurry_zero {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [] [(i : ι) → (j : α i) → Zero (δ i j)] :
@[simp]
theorem DFinsupp.sigmaCurry_add {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [] [(i : ι) → (j : α i) → AddZeroClass (δ i j)] (f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd) (g : Π₀ (i : (x : ι) × α x), δ i.fst i.snd) :
(f + g).sigmaCurry = f.sigmaCurry + g.sigmaCurry
@[simp]
theorem DFinsupp.sigmaCurry_smul {ι : Type u} {γ : Type w} {α : ιType u_2} {δ : (i : ι) → α iType v} [] [] [(i : ι) → (j : α i) → AddMonoid (δ i j)] [(i : ι) → (j : α i) → DistribMulAction γ (δ i j)] (r : γ) (f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd) :
(r f).sigmaCurry = r f.sigmaCurry
@[simp]
theorem DFinsupp.sigmaCurry_single {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [] [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → Zero (δ i j)] (ij : (i : ι) × α i) (x : δ ij.fst ij.snd) :
(DFinsupp.single ij x).sigmaCurry = DFinsupp.single ij.fst (DFinsupp.single ij.snd x)
def DFinsupp.sigmaUncurry {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [(i : ι) → (j : α i) → Zero (δ i j)] [] (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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem DFinsupp.sigmaUncurry_apply {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [] [(i : ι) → (j : α i) → Zero (δ i j)] (f : Π₀ (i : ι) (j : α i), δ i j) (i : ι) (j : α i) :
f.sigmaUncurry i, j = (f i) j
@[simp]
theorem DFinsupp.sigmaUncurry_zero {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [] [(i : ι) → (j : α i) → Zero (δ i j)] :
@[simp]
theorem DFinsupp.sigmaUncurry_add {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [] [(i : ι) → (j : α i) → AddZeroClass (δ i j)] (f : Π₀ (i : ι) (j : α i), δ i j) (g : Π₀ (i : ι) (j : α i), δ i j) :
(f + g).sigmaUncurry = f.sigmaUncurry + g.sigmaUncurry
@[simp]
theorem DFinsupp.sigmaUncurry_smul {ι : Type u} {γ : Type w} {α : ιType u_2} {δ : (i : ι) → α iType v} [] [] [(i : ι) → (j : α i) → AddMonoid (δ i j)] [(i : ι) → (j : α i) → DistribMulAction γ (δ i j)] (r : γ) (f : Π₀ (i : ι) (j : α i), δ i j) :
(r f).sigmaUncurry = r f.sigmaUncurry
@[simp]
theorem DFinsupp.sigmaUncurry_single {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [] [(i : ι) → (j : α i) → Zero (δ i j)] [(i : ι) → DecidableEq (α i)] (i : ι) (j : α i) (x : δ i j) :
(DFinsupp.single i (DFinsupp.single j x)).sigmaUncurry = DFinsupp.single i, j x
def DFinsupp.sigmaCurryEquiv {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [(i : ι) → (j : α i) → Zero (δ i j)] [] :
(Π₀ (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.piCurry.

Equations
• DFinsupp.sigmaCurryEquiv = { toFun := DFinsupp.sigmaCurry, invFun := DFinsupp.sigmaUncurry, left_inv := , right_inv := }
Instances For
def DFinsupp.extendWith {ι : Type u} {α : Type v} [(i : ) → Zero (α i)] (a : α none) (f : Π₀ (i : ι), α (some i)) :
Π₀ (i : ), α i

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

This is the dfinsupp version of Option.rec.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem DFinsupp.extendWith_none {ι : Type u} {α : Type v} [(i : ) → Zero (α i)] (f : Π₀ (i : ι), α (some i)) (a : α none) :
none = a
@[simp]
theorem DFinsupp.extendWith_some {ι : Type u} {α : Type v} [(i : ) → Zero (α i)] (f : Π₀ (i : ι), α (some i)) (a : α none) (i : ι) :
(some i) = f i
@[simp]
theorem DFinsupp.extendWith_single_zero {ι : Type u} {α : Type v} [] [(i : ) → Zero (α i)] (i : ι) (x : α (some i)) :
@[simp]
theorem DFinsupp.extendWith_zero {ι : Type u} {α : Type v} [] [(i : ) → Zero (α i)] (x : α none) :
@[simp]
theorem DFinsupp.equivProdDFinsupp_apply {ι : Type u} {α : Type v} [(i : ) → Zero (α i)] (f : Π₀ (i : ), α i) :
DFinsupp.equivProdDFinsupp f = (f none, DFinsupp.comapDomain some f)
@[simp]
theorem DFinsupp.equivProdDFinsupp_symm_apply {ι : Type u} {α : Type v} [(i : ) → Zero (α i)] (f : α none × Π₀ (i : ι), α (some i)) :
DFinsupp.equivProdDFinsupp.symm f = DFinsupp.extendWith f.1 f.2
noncomputable def DFinsupp.equivProdDFinsupp {ι : Type u} {α : Type v} [(i : ) → Zero (α i)] :
(Π₀ (i : ), α i) α none × Π₀ (i : ι), α (some i)

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

This is the dfinsupp version of Equiv.piOptionEquivProd.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem DFinsupp.equivProdDFinsupp_add {ι : Type u} {α : Type v} [(i : ) → AddZeroClass (α i)] (f : Π₀ (i : ), α i) (g : Π₀ (i : ), α i) :
DFinsupp.equivProdDFinsupp (f + g) = DFinsupp.equivProdDFinsupp f + DFinsupp.equivProdDFinsupp g
theorem DFinsupp.equivProdDFinsupp_smul {ι : Type u} {γ : Type w} {α : Type v} [] [(i : ) → AddMonoid (α i)] [(i : ) → DistribMulAction γ (α i)] (r : γ) (f : Π₀ (i : ), α i) :
DFinsupp.equivProdDFinsupp (r f) = r DFinsupp.equivProdDFinsupp f
def DFinsupp.sum {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → 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
• f.sum g = if.support, g i (f i)
Instances For
def DFinsupp.prod {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] (f : Π₀ (i : ι), β i) (g : (i : ι) → β iγ) :
γ

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

Equations
• f.prod g = if.support, g i (f i)
Instances For
@[simp]
theorem map_dfinsupp_sum {ι : Type u} {β : ιType v} [] {R : Type u_1} {S : Type u_2} {H : Type u_3} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] [] [FunLike H R S] [] (h : H) (f : Π₀ (i : ι), β i) (g : (i : ι) → β iR) :
h (f.sum g) = f.sum fun (a : ι) (b : β a) => h (g a b)
@[simp]
theorem map_dfinsupp_prod {ι : Type u} {β : ιType v} [] {R : Type u_1} {S : Type u_2} {H : Type u_3} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] [] [FunLike H R S] [] (h : H) (f : Π₀ (i : ι), β i) (g : (i : ι) → β iR) :
h (f.prod g) = f.prod fun (a : ι) (b : β a) => h (g a b)
theorem DFinsupp.sum_mapRange_index {ι : Type u} {γ : Type w} [] {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → Zero (β₁ i)] [(i : ι) → 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) :
(DFinsupp.mapRange f hf g).sum h = g.sum fun (i : ι) (b : β₁ i) => h i (f i b)
theorem DFinsupp.prod_mapRange_index {ι : Type u} {γ : Type w} [] {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → Zero (β₁ i)] [(i : ι) → 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 = 1) :
(DFinsupp.mapRange f hf g).prod h = g.prod fun (i : ι) (b : β₁ i) => h i (f i b)
theorem DFinsupp.sum_zero_index {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {h : (i : ι) → β iγ} :
= 0
theorem DFinsupp.prod_zero_index {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {h : (i : ι) → β iγ} :
= 1
theorem DFinsupp.sum_single_index {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {i : ι} {b : β i} {h : (i : ι) → β iγ} (h_zero : h i 0 = 0) :
(DFinsupp.single i b).sum h = h i b
theorem DFinsupp.prod_single_index {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {i : ι} {b : β i} {h : (i : ι) → β iγ} (h_zero : h i 0 = 1) :
(DFinsupp.single i b).prod h = h i b
theorem DFinsupp.sum_neg_index {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddGroup (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {g : Π₀ (i : ι), β i} {h : (i : ι) → β iγ} (h0 : ∀ (i : ι), h i 0 = 0) :
(-g).sum h = g.sum fun (i : ι) (b : β i) => h i (-b)
theorem DFinsupp.prod_neg_index {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddGroup (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {g : Π₀ (i : ι), β i} {h : (i : ι) → β iγ} (h0 : ∀ (i : ι), h i 0 = 1) :
(-g).prod h = g.prod fun (i : ι) (b : β i) => h i (-b)
theorem DFinsupp.sum_comm {γ : Type w} {ι₁ : Type u_3} {ι₂ : Type u_4} {β₁ : ι₁Type u_1} {β₂ : ι₂Type u_2} [] [] [(i : ι₁) → Zero (β₁ i)] [(i : ι₂) → 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 fun (i₁ : ι₁) (x₁ : β₁ i₁) => f₂.sum fun (i₂ : ι₂) (x₂ : β₂ i₂) => h i₁ x₁ i₂ x₂) = f₂.sum fun (i₂ : ι₂) (x₂ : β₂ i₂) => f₁.sum fun (i₁ : ι₁) (x₁ : β₁ i₁) => h i₁ x₁ i₂ x₂
theorem DFinsupp.prod_comm {γ : Type w} {ι₁ : Type u_3} {ι₂ : Type u_4} {β₁ : ι₁Type u_1} {β₂ : ι₂Type u_2} [] [] [(i : ι₁) → Zero (β₁ i)] [(i : ι₂) → 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₁.prod fun (i₁ : ι₁) (x₁ : β₁ i₁) => f₂.prod fun (i₂ : ι₂) (x₂ : β₂ i₂) => h i₁ x₁ i₂ x₂) = f₂.prod fun (i₂ : ι₂) (x₂ : β₂ i₂) => f₁.prod fun (i₁ : ι₁) (x₁ : β₁ i₁) => h i₁ x₁ i₂ x₂
@[simp]
theorem DFinsupp.sum_apply {ι : Type u_1} {β : ιType v} {ι₁ : Type u₁} [] {β₁ : ι₁Type v₁} [(i₁ : ι₁) → Zero (β₁ i₁)] [(i : ι₁) → (x : β₁ i) → Decidable (x 0)] [(i : ι) → AddCommMonoid (β i)] {f : Π₀ (i₁ : ι₁), β₁ i₁} {g : (i₁ : ι₁) → β₁ i₁Π₀ (i : ι), β i} {i₂ : ι} :
(f.sum g) i₂ = f.sum fun (i₁ : ι₁) (b : β₁ i₁) => (g i₁ b) i₂
theorem DFinsupp.support_sum {ι : Type u} {β : ιType v} [] {ι₁ : Type u₁} [] {β₁ : ι₁Type v₁} [(i₁ : ι₁) → Zero (β₁ i₁)] [(i : ι₁) → (x : β₁ i) → Decidable (x 0)] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] {f : Π₀ (i₁ : ι₁), β₁ i₁} {g : (i₁ : ι₁) → β₁ i₁Π₀ (i : ι), β i} :
(f.sum g).support f.support.biUnion fun (i : ι₁) => (g i (f i)).support
@[simp]
theorem DFinsupp.sum_zero {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {f : Π₀ (i : ι), β i} :
(f.sum fun (x : ι) (x : β x) => 0) = 0
@[simp]
theorem DFinsupp.prod_one {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {f : Π₀ (i : ι), β i} :
(f.prod fun (x : ι) (x : β x) => 1) = 1
@[simp]
theorem DFinsupp.sum_add {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {f : Π₀ (i : ι), β i} {h₁ : (i : ι) → β iγ} {h₂ : (i : ι) → β iγ} :
(f.sum fun (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} [] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {f : Π₀ (i : ι), β i} {h₁ : (i : ι) → β iγ} {h₂ : (i : ι) → β iγ} :
(f.prod fun (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} [] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {f : Π₀ (i : ι), β i} {h : (i : ι) → β iγ} :
(f.sum fun (i : ι) (b : β i) => -h i b) = -f.sum h
@[simp]
theorem DFinsupp.prod_inv {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {f : Π₀ (i : ι), β i} {h : (i : ι) → β iγ} :
(f.prod fun (i : ι) (b : β i) => (h i b)⁻¹) = (f.prod h)⁻¹
theorem DFinsupp.sum_eq_zero {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → 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} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {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} [] {α : Type u_1} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] [] {f : Π₀ (i : ι), β i} {h : (i : ι) → β iγ} {c : α} :
c f.sum h = f.sum fun (a : ι) (b : β a) => c h a b
theorem DFinsupp.sum_add_index {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {f : Π₀ (i : ι), β i} {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} [] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {f : Π₀ (i : ι), β i} {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_sum_mem {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {S : Type u_1} [SetLike S γ] [] (s : S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β iγ) (h : ∀ (c : ι), f c 0g c (f c) s) :
f.sum g s
theorem dfinsupp_prod_mem {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {S : Type u_1} [SetLike S γ] [] (s : S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β iγ) (h : ∀ (c : ι), f c 0g c (f c) s) :
f.prod g s
@[simp]
theorem DFinsupp.sum_eq_sum_fintype {ι : Type u} {γ : Type w} {β : ιType v} [] [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] (v : Π₀ (i : ι), β i) {f : (i : ι) → β iγ} (hf : ∀ (i : ι), f i 0 = 0) :
v.sum f = i : ι, f i (DFinsupp.equivFunOnFintype v i)
@[simp]
theorem DFinsupp.prod_eq_prod_fintype {ι : Type u} {γ : Type w} {β : ιType v} [] [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] (v : Π₀ (i : ι), β i) {f : (i : ι) → β iγ} (hf : ∀ (i : ι), f i 0 = 1) :
v.prod f = i : ι, f i (DFinsupp.equivFunOnFintype v i)
@[simp]
theorem DFinsupp.prod_eq_zero_iff {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → Zero (β i)] [] [] [(i : ι) → DecidableEq (β i)] {f : Π₀ (i : ι), β i} {g : (i : ι) → β iγ} :
f.prod g = 0 if.support, g i (f i) = 0
theorem DFinsupp.prod_ne_zero_iff {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → Zero (β i)] [] [] [(i : ι) → DecidableEq (β i)] {f : Π₀ (i : ι), β i} {g : (i : ι) → β iγ} :
f.prod g 0 if.support, g i (f i) 0
def DFinsupp.sumAddHom {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] [] (φ : (i : ι) → β i →+ γ) :
(Π₀ (i : ι), β i) →+ γ

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem DFinsupp.sumAddHom_single {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] [] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i) :
(DFinsupp.single i x) = (φ i) x
@[simp]
theorem DFinsupp.sumAddHom_comp_single {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] [] (f : (i : ι) → β i →+ γ) (i : ι) :
.comp = f i
theorem DFinsupp.sumAddHom_apply {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] (φ : (i : ι) → β i →+ γ) (f : Π₀ (i : ι), β i) :
f = f.sum fun (x : ι) => (φ x)

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

theorem dfinsupp_sumAddHom_mem {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] [] {S : Type u_1} [SetLike S γ] [] (s : S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ γ) (h : ∀ (c : ι), f c 0(g c) (f c) s) :
f s
theorem AddSubmonoid.iSup_eq_mrange_dfinsupp_sumAddHom {ι : Type u} {γ : Type w} [] [] (S : ι) :
iSup S = AddMonoidHom.mrange (DFinsupp.sumAddHom fun (i : ι) => (S i).subtype)

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

theorem AddSubmonoid.bsupr_eq_mrange_dfinsupp_sumAddHom {ι : Type u} {γ : Type w} [] (p : ιProp) [] [] (S : ι) :
⨆ (i : ι), ⨆ (_ : p i), S i = AddMonoidHom.mrange ((DFinsupp.sumAddHom fun (i : ι) => (S i).subtype).comp (DFinsupp.filterAddMonoidHom (fun (i : ι) => (S i)) p))

The bounded supremum of a family of commutative additive submonoids is equal to the range of DFinsupp.sumAddHom composed with DFinsupp.filterAddMonoidHom; that is, every element in the bounded iSup 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.

theorem AddSubmonoid.mem_iSup_iff_exists_dfinsupp {ι : Type u} {γ : Type w} [] [] (S : ι) (x : γ) :
x iSup S ∃ (f : Π₀ (i : ι), (S i)), (DFinsupp.sumAddHom fun (i : ι) => (S i).subtype) f = x
theorem AddSubmonoid.mem_iSup_iff_exists_dfinsupp' {ι : Type u} {γ : Type w} [] [] (S : ι) [(i : ι) → (x : (S i)) → Decidable (x 0)] (x : γ) :
x iSup S ∃ (f : Π₀ (i : ι), (S i)), (f.sum fun (i : ι) (xi : (S i)) => xi) = x

A variant of AddSubmonoid.mem_iSup_iff_exists_dfinsupp with the RHS fully unfolded.

theorem AddSubmonoid.mem_bsupr_iff_exists_dfinsupp {ι : Type u} {γ : Type w} [] (p : ιProp) [] [] (S : ι) (x : γ) :
x ⨆ (i : ι), ⨆ (_ : p i), S i ∃ (f : Π₀ (i : ι), (S i)), (DFinsupp.sumAddHom fun (i : ι) => (S i).subtype) (DFinsupp.filter p f) = x
theorem DFinsupp.sumAddHom_comm {ι₁ : Type u_4} {ι₂ : Type u_5} {β₁ : ι₁Type u_1} {β₂ : ι₂Type u_2} {γ : Type u_3} [] [] [(i : ι₁) → AddZeroClass (β₁ i)] [(i : ι₂) → AddZeroClass (β₂ i)] [] (f₁ : Π₀ (i : ι₁), β₁ i) (f₂ : Π₀ (i : ι₂), β₂ i) (h : (i : ι₁) → (j : ι₂) → β₁ i →+ β₂ j →+ γ) :
(DFinsupp.sumAddHom fun (i₂ : ι₂) => (DFinsupp.sumAddHom fun (i₁ : ι₁) => h i₁ i₂) f₁) f₂ = (DFinsupp.sumAddHom fun (i₁ : ι₁) => (DFinsupp.sumAddHom fun (i₂ : ι₂) => (h i₁ i₂).flip) f₂) f₁
@[simp]
theorem DFinsupp.liftAddHom_apply {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] [] (φ : (i : ι) → β i →+ γ) :
@[simp]
theorem DFinsupp.liftAddHom_symm_apply {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] [] (F : (Π₀ (i : ι), β i) →+ γ) (i : ι) :
DFinsupp.liftAddHom.symm F i = F.comp
def DFinsupp.liftAddHom {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] [] :
((i : ι) → β i →+ γ) ≃+ ((Π₀ (i : ι), β i) →+ γ)

The DFinsupp version of Finsupp.liftAddHom,

Equations
• DFinsupp.liftAddHom = { toFun := DFinsupp.sumAddHom, invFun := fun (F : (Π₀ (i : ι), β i) →+ γ) (i : ι) => F.comp , left_inv := , right_inv := , map_add' := }
Instances For
@[simp]
theorem DFinsupp.liftAddHom_singleAddHom {ι : Type u} {β : ιType v} [] [(i : ι) → AddCommMonoid (β i)] :
DFinsupp.liftAddHom = AddMonoidHom.id (Π₀ (i : ι), β i)

The DFinsupp version of Finsupp.liftAddHom_singleAddHom,

theorem DFinsupp.liftAddHom_apply_single {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] [] (f : (i : ι) → β i →+ γ) (i : ι) (x : β i) :
(DFinsupp.liftAddHom f) (DFinsupp.single i x) = (f i) x

The DFinsupp version of Finsupp.liftAddHom_apply_single,

theorem DFinsupp.liftAddHom_comp_single {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] [] (f : (i : ι) → β i →+ γ) (i : ι) :
(DFinsupp.liftAddHom f).comp = f i

The DFinsupp version of Finsupp.liftAddHom_comp_single,

theorem DFinsupp.comp_liftAddHom {ι : Type u} {γ : Type w} {β : ιType v} [] {δ : Type u_1} [(i : ι) → AddZeroClass (β i)] [] [] (g : γ →+ δ) (f : (i : ι) → β i →+ γ) :
g.comp (DFinsupp.liftAddHom f) = DFinsupp.liftAddHom fun (a : ι) => g.comp (f a)

The DFinsupp version of Finsupp.comp_liftAddHom,

@[simp]
theorem DFinsupp.sumAddHom_zero {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] [] :
(DFinsupp.sumAddHom fun (i : ι) => 0) = 0
@[simp]
theorem DFinsupp.sumAddHom_add {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddZeroClass (β i)] [] (g : (i : ι) → β i →+ γ) (h : (i : ι) → β i →+ γ) :
(DFinsupp.sumAddHom fun (i : ι) => g i + h i) =
@[simp]
theorem DFinsupp.sumAddHom_singleAddHom {ι : Type u} {β : ιType v} [] [(i : ι) → AddCommMonoid (β i)] :
= AddMonoidHom.id (Π₀ (i : ι), β i)
theorem DFinsupp.comp_sumAddHom {ι : Type u} {γ : Type w} {β : ιType v} [] {δ : Type u_1} [(i : ι) → AddZeroClass (β i)] [] [] (g : γ →+ δ) (f : (i : ι) → β i →+ γ) :
g.comp = DFinsupp.sumAddHom fun (a : ι) => g.comp (f a)
theorem DFinsupp.sum_sub_index {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → AddGroup (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {f : Π₀ (i : ι), β i} {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
theorem DFinsupp.sum_finset_sum_index {ι : Type u} {β : ιType v} [] {γ : Type w} {α : Type x} [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {s : } {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₂) :
is, (g i).sum h = (∑ is, g i).sum h
theorem DFinsupp.prod_finset_sum_index {ι : Type u} {β : ιType v} [] {γ : Type w} {α : Type x} [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {s : } {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₂) :
is, (g i).prod h = (∑ is, g i).prod h
theorem DFinsupp.sum_sum_index {ι : Type u} {γ : Type w} {β : ιType v} [] {ι₁ : Type u₁} [] {β₁ : ι₁Type v₁} [(i₁ : ι₁) → Zero (β₁ i₁)] [(i : ι₁) → (x : β₁ i) → Decidable (x 0)] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {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 fun (i : ι₁) (b : β₁ i) => (g i b).sum h
theorem DFinsupp.prod_sum_index {ι : Type u} {γ : Type w} {β : ιType v} [] {ι₁ : Type u₁} [] {β₁ : ι₁Type v₁} [(i₁ : ι₁) → Zero (β₁ i₁)] [(i : ι₁) → (x : β₁ i) → Decidable (x 0)] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {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 fun (i : ι₁) (b : β₁ i) => (g i b).prod h
@[simp]
theorem DFinsupp.sum_single {ι : Type u} {β : ιType v} [] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] {f : Π₀ (i : ι), β i} :
f.sum DFinsupp.single = f
theorem DFinsupp.sum_subtypeDomain_index {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {v : Π₀ (i : ι), β i} {p : ιProp} [] {h : (i : ι) → β iγ} (hp : xv.support, p x) :
(.sum fun (i : ) (b : β i) => h (↑i) b) = v.sum h
theorem DFinsupp.prod_subtypeDomain_index {ι : Type u} {γ : Type w} {β : ιType v} [] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] {v : Π₀ (i : ι), β i} {p : ιProp} [] {h : (i : ι) → β iγ} (hp : xv.support, p x) :
(.prod fun (i : ) (b : β i) => h (↑i) b) = v.prod h
theorem DFinsupp.subtypeDomain_sum {γ : Type w} {ι : Type u_1} {β : ιType v} [(i : ι) → AddCommMonoid (β i)] {s : } {h : γΠ₀ (i : ι), β i} {p : ιProp} [] :
DFinsupp.subtypeDomain p (∑ cs, h c) = cs, DFinsupp.subtypeDomain p (h c)
theorem DFinsupp.subtypeDomain_finsupp_sum {γ : Type w} {ι : Type u_1} {β : ιType v} {δ : γType x} [] [(c : γ) → Zero (δ c)] [(c : γ) → (x : δ c) → Decidable (x 0)] [(i : ι) → AddCommMonoid (β i)] {p : ιProp} [] {s : Π₀ (c : γ), δ c} {h : (c : γ) → δ cΠ₀ (i : ι), β i} :
DFinsupp.subtypeDomain p (s.sum h) = s.sum fun (c : γ) (d : δ c) => DFinsupp.subtypeDomain p (h c d)

### Bundled versions of DFinsupp.mapRange#

The names should match the equivalent bundled Finsupp.mapRange definitions.

theorem DFinsupp.mapRange_add {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → AddZeroClass (β₁ i)] [(i : ι) → AddZeroClass (β₂ 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₁ : Π₀ (i : ι), β₁ i) (g₂ : Π₀ (i : ι), β₁ i) :
DFinsupp.mapRange f hf (g₁ + g₂) = DFinsupp.mapRange f hf g₁ + DFinsupp.mapRange f hf g₂
@[simp]
theorem DFinsupp.mapRange.addMonoidHom_apply {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → AddZeroClass (β₁ i)] [(i : ι) → AddZeroClass (β₂ i)] (f : (i : ι) → β₁ i →+ β₂ i) (x : Π₀ (i : ι), β₁ i) :
= DFinsupp.mapRange (fun (i : ι) (x : β₁ i) => (f i) x) x
def DFinsupp.mapRange.addMonoidHom {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → AddZeroClass (β₁ i)] [(i : ι) → AddZeroClass (β₂ i)] (f : (i : ι) → β₁ i →+ β₂ i) :
(Π₀ (i : ι), β₁ i) →+ Π₀ (i : ι), β₂ i

DFinsupp.mapRange as an AddMonoidHom.

Equations
• = { toFun := DFinsupp.mapRange (fun (i : ι) (x : β₁ i) => (f i) x) , map_zero' := , map_add' := }
Instances For
@[simp]
theorem DFinsupp.mapRange.addMonoidHom_id {ι : Type u} {β₂ : ιType v₂} [(i : ι) → AddZeroClass (β₂ i)] :
(DFinsupp.mapRange.addMonoidHom fun (i : ι) => AddMonoidHom.id (β₂ i)) = AddMonoidHom.id (Π₀ (i : ι), β₂ i)
theorem DFinsupp.mapRange.addMonoidHom_comp {ι : Type u} {β : ιType v} {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → AddZeroClass (β i)] [(i : ι) → AddZeroClass (β₁ i)] [(i : ι) → AddZeroClass (β₂ i)] (f : (i : ι) → β₁ i →+ β₂ i) (f₂ : (i : ι) → β i →+ β₁ i) :
(DFinsupp.mapRange.addMonoidHom fun (i : ι) => (f i).comp (f₂ i)) =
@[simp]
theorem DFinsupp.mapRange.addEquiv_apply {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → AddZeroClass (β₁ i)] [(i : ι) → AddZeroClass (β₂ i)] (e : (i : ι) → β₁ i ≃+ β₂ i) (x : Π₀ (i : ι), β₁ i) :
= DFinsupp.mapRange (fun (i : ι) (x : β₁ i) => (e i) x) x
def DFinsupp.mapRange.addEquiv {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → AddZeroClass (β₁ i)] [(i : ι) → AddZeroClass (β₂ i)] (e : (i : ι) → β₁ i ≃+ β₂ i) :
(Π₀ (i : ι), β₁ i) ≃+ Π₀ (i : ι), β₂ i

DFinsupp.mapRange.addMonoidHom as an AddEquiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem DFinsupp.mapRange.addEquiv_refl {ι : Type u} {β₁ : ιType v₁} [(i : ι) → AddZeroClass (β₁ i)] :
(DFinsupp.mapRange.addEquiv fun (i : ι) => AddEquiv.refl (β₁ i)) = AddEquiv.refl (Π₀ (i : ι), β₁ i)
theorem DFinsupp.mapRange.addEquiv_trans {ι : Type u} {β : ιType v} {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → AddZeroClass (β i)] [(i : ι) → AddZeroClass (β₁ i)] [(i : ι) → AddZeroClass (β₂ i)] (f : (i : ι) → β i ≃+ β₁ i) (f₂ : (i : ι) → β₁ i ≃+ β₂ i) :
(DFinsupp.mapRange.addEquiv fun (i : ι) => (f i).trans (f₂ i)) = .trans
@[simp]
theorem DFinsupp.mapRange.addEquiv_symm {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → AddZeroClass (β₁ i)] [(i : ι) → AddZeroClass (β₂ i)] (e : (i : ι) → β₁ i ≃+ β₂ i) :
.symm = DFinsupp.mapRange.addEquiv fun (i : ι) => (e i).symm

### Product and sum lemmas for bundled morphisms. #

In this section, we provide analogues of AddMonoidHom.map_sum, AddMonoidHom.coe_finset_sum, and AddMonoidHom.finset_sum_apply for DFinsupp.sum and DFinsupp.sumAddHom instead of Finset.sum.

We provide these for AddMonoidHom, MonoidHom, RingHom, AddEquiv, and MulEquiv.

Lemmas for LinearMap and LinearEquiv are in another file.

@[simp]
theorem AddMonoidHom.coe_dfinsupp_sum {ι : Type u} {β : ιType v} [] {R : Type u_1} {S : Type u_2} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] [] (f : Π₀ (i : ι), β i) (g : (i : ι) → β iR →+ S) :
(f.sum g) = f.sum fun (a : ι) (b : β a) => (g a b)
@[simp]
theorem MonoidHom.coe_dfinsupp_prod {ι : Type u} {β : ιType v} [] {R : Type u_1} {S : Type u_2} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] [] (f : Π₀ (i : ι), β i) (g : (i : ι) → β iR →* S) :
(f.prod g) = f.prod fun (a : ι) (b : β a) => (g a b)
theorem AddMonoidHom.dfinsupp_sum_apply {ι : Type u} {β : ιType v} [] {R : Type u_1} {S : Type u_2} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] [] (f : Π₀ (i : ι), β i) (g : (i : ι) → β iR →+ S) (r : R) :
(f.sum g) r = f.sum fun (a : ι) (b : β a) => (g a b) r
theorem MonoidHom.dfinsupp_prod_apply {ι : Type u} {β : ιType v} [] {R : Type u_1} {S : Type u_2} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] [] [] (f : Π₀ (i : ι), β i) (g : (i : ι) → β iR →* S) (r : R) :
(f.prod g) r = f.prod fun (a : ι) (b : β a) => (g a b) r

The above lemmas, repeated for DFinsupp.sumAddHom.

@[simp]
theorem AddMonoidHom.map_dfinsupp_sumAddHom {ι : Type u} {β : ιType v} [] {R : Type u_1} {S : Type u_2} [] [] [(i : ι) → AddZeroClass (β i)] (h : R