# Documentation

Mathlib.Data.Dfinsupp.Basic

# 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 (λ 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) [inst : (i : ι) → Zero (β i)] :
Type (maxuv)
• mk' :: (
• The underlying function of a dependent function with finite support (aka Dfinsupp).

toFun : (i : ι) → β i
• The support of a dependent function with finite support (aka Dfinsupp).

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

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

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

Instances For

Π₀ 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.

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.

Equations
instance Dfinsupp.funLike {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] :
FunLike (Dfinsupp fun i => β i) ι β
Equations
• Dfinsupp.funLike = { coe := fun f => f.toFun, coe_injective' := (_ : ∀ (x x_1 : Dfinsupp fun i => β i), (fun f => f.toFun) x = (fun f => f.toFun) x_1x = x_1) }
instance Dfinsupp.instCoeFunDfinsuppForAll {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] :
CoeFun (Dfinsupp fun i => β i) fun x => (i : ι) → β i

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

Equations
• Dfinsupp.instCoeFunDfinsuppForAll = inferInstance
@[simp]
theorem Dfinsupp.toFun_eq_coe {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] (f : Dfinsupp fun i => β i) :
f.toFun = f
theorem Dfinsupp.ext {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] {f : Dfinsupp fun i => β i} {g : Dfinsupp fun i => β i} (h : ∀ (i : ι), f i = g i) :
f = g
theorem Dfinsupp.ext_iff {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] {f : Dfinsupp fun i => β i} {g : Dfinsupp fun i => β i} :
f = g ∀ (i : ι), f i = g i
theorem Dfinsupp.coeFn_injective {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] :
Function.Injective FunLike.coe
instance Dfinsupp.instZeroDfinsupp {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] :
Zero (Dfinsupp fun i => β i)
Equations
• One or more equations did not get rendered due to their size.
instance Dfinsupp.instInhabitedDfinsupp {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] :
Inhabited (Dfinsupp fun i => β i)
Equations
• Dfinsupp.instInhabitedDfinsupp = { default := 0 }
@[simp]
theorem Dfinsupp.coe_mk' {ι : Type u} {β : ιType v} [inst : (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} [inst : (i : ι) → Zero (β i)] :
0 = 0
theorem Dfinsupp.zero_apply {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] (i : ι) :
0 i = 0
def Dfinsupp.mapRange {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [inst : (i : ι) → Zero (β₁ i)] [inst : (i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ iβ₂ i) (hf : ∀ (i : ι), f i 0 = 0) (x : Dfinsupp fun i => β₁ i) :
Dfinsupp fun 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
• One or more equations did not get rendered due to their size.
@[simp]
theorem Dfinsupp.mapRange_apply {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [inst : (i : ι) → Zero (β₁ i)] [inst : (i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ iβ₂ i) (hf : ∀ (i : ι), f i 0 = 0) (g : Dfinsupp fun i => β₁ i) (i : ι) :
↑() i = f i (g i)
@[simp]
theorem Dfinsupp.mapRange_id {ι : Type u} {β₁ : ιType v₁} [inst : (i : ι) → Zero (β₁ i)] (h : optParam (∀ (i : ι), id 0 = 0) (_ : ∀ (i : ι), id 0 = id 0)) (g : Dfinsupp fun i => β₁ i) :
Dfinsupp.mapRange (fun i => id) h g = g
theorem Dfinsupp.mapRange_comp {ι : Type u} {β : ιType v} {β₁ : ιType v₁} {β₂ : ιType v₂} [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → Zero (β₁ i)] [inst : (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 : Dfinsupp fun 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₂} [inst : (i : ι) → Zero (β₁ i)] [inst : (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₂} [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → Zero (β₁ i)] [inst : (i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ iβ₂ iβ i) (hf : ∀ (i : ι), f i 0 0 = 0) (x : Dfinsupp fun i => β₁ i) (y : Dfinsupp fun i => β₂ i) :
Dfinsupp fun i => β i

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

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Dfinsupp.zipWith_apply {ι : Type u} {β : ιType v} {β₁ : ιType v₁} {β₂ : ιType v₂} [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → Zero (β₁ i)] [inst : (i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ iβ₂ iβ i) (hf : ∀ (i : ι), f i 0 0 = 0) (g₁ : Dfinsupp fun i => β₁ i) (g₂ : Dfinsupp fun i => β₂ i) (i : ι) :
↑(Dfinsupp.zipWith f hf g₁ g₂) i = f i (g₁ i) (g₂ i)
def Dfinsupp.piecewise {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] (x : Dfinsupp fun i => β i) (y : Dfinsupp fun i => β i) (s : Set ι) [inst : (i : ι) → Decidable (i s)] :
Dfinsupp fun 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} [inst : (i : ι) → Zero (β i)] (x : Dfinsupp fun i => β i) (y : Dfinsupp fun i => β i) (s : Set ι) [inst : (i : ι) → Decidable (i s)] (i : ι) :
↑() i = if i s then x i else y i
@[simp]
theorem Dfinsupp.coe_piecewise {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] (x : Dfinsupp fun i => β i) (y : Dfinsupp fun i => β i) (s : Set ι) [inst : (i : ι) → Decidable (i s)] :
↑() = Set.piecewise s x y
instance Dfinsupp.instAddDfinsuppToZero {ι : Type u} {β : ιType v} [inst : (i : ι) → AddZeroClass (β i)] :
Add (Dfinsupp fun i => β i)
Equations
• Dfinsupp.instAddDfinsuppToZero = { add := Dfinsupp.zipWith (fun x x_1 x_2 => x_1 + x_2) (_ : ∀ (x : ι), 0 + 0 = 0) }
theorem Dfinsupp.add_apply {ι : Type u} {β : ιType v} [inst : (i : ι) → AddZeroClass (β i)] (g₁ : Dfinsupp fun i => β i) (g₂ : Dfinsupp fun i => β i) (i : ι) :
↑(g₁ + g₂) i = g₁ i + g₂ i
@[simp]
theorem Dfinsupp.coe_add {ι : Type u} {β : ιType v} [inst : (i : ι) → AddZeroClass (β i)] (g₁ : Dfinsupp fun i => β i) (g₂ : Dfinsupp fun i => β i) :
↑(g₁ + g₂) = g₁ + g₂
instance Dfinsupp.addZeroClass {ι : Type u} {β : ιType v} [inst : (i : ι) → AddZeroClass (β i)] :
AddZeroClass (Dfinsupp fun i => β i)
Equations
instance Dfinsupp.hasNatScalar {ι : Type u} {β : ιType v} [inst : (i : ι) → AddMonoid (β i)] :
SMul (Dfinsupp fun 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 => Dfinsupp.mapRange (fun x => (fun x_1 x_2 => x_1 x_2) c) (_ : ∀ (x : ι), c 0 = 0) v }
theorem Dfinsupp.nsmul_apply {ι : Type u} {β : ιType v} [inst : (i : ι) → AddMonoid (β i)] (b : ) (v : Dfinsupp fun i => β i) (i : ι) :
↑(b v) i = b v i
@[simp]
theorem Dfinsupp.coe_nsmul {ι : Type u} {β : ιType v} [inst : (i : ι) → AddMonoid (β i)] (b : ) (v : Dfinsupp fun i => β i) :
↑(b v) = b v
instance Dfinsupp.instAddMonoidDfinsuppToZero {ι : Type u} {β : ιType v} [inst : (i : ι) → AddMonoid (β i)] :
AddMonoid (Dfinsupp fun i => β i)
Equations
• One or more equations did not get rendered due to their size.
def Dfinsupp.coeFnAddMonoidHom {ι : Type u} {β : ιType v} [inst : (i : ι) → AddZeroClass (β i)] :
(Dfinsupp fun i => β i) →+ (i : ι) → β i

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

Equations
• Dfinsupp.coeFnAddMonoidHom = { toZeroHom := { toFun := FunLike.coe, map_zero' := (_ : 0 = 0) }, map_add' := (_ : ∀ (g₁ g₂ : Dfinsupp fun i => β i), ↑(g₁ + g₂) = g₁ + g₂) }
def Dfinsupp.evalAddMonoidHom {ι : Type u} {β : ιType v} [inst : (i : ι) → AddZeroClass (β i)] (i : ι) :
(Dfinsupp fun i => β i) →+ β i

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

Equations
instance Dfinsupp.instAddCommMonoidDfinsuppToZeroToAddMonoid {ι : Type u} {β : ιType v} [inst : (i : ι) → AddCommMonoid (β i)] :
AddCommMonoid (Dfinsupp fun i => β i)
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Dfinsupp.coe_finset_sum {ι : Type u} {β : ιType v} {α : Type u_1} [inst : (i : ι) → AddCommMonoid (β i)] (s : ) (g : αDfinsupp fun i => β i) :
↑(Finset.sum s fun a => g a) = Finset.sum s fun a => ↑(g a)
@[simp]
theorem Dfinsupp.finset_sum_apply {ι : Type u} {β : ιType v} {α : Type u_1} [inst : (i : ι) → AddCommMonoid (β i)] (s : ) (g : αDfinsupp fun i => β i) (i : ι) :
↑(Finset.sum s fun a => g a) i = Finset.sum s fun a => ↑(g a) i
instance Dfinsupp.instNegDfinsuppToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoid {ι : Type u} {β : ιType v} [inst : (i : ι) → AddGroup (β i)] :
Neg (Dfinsupp fun i => β i)
Equations
• Dfinsupp.instNegDfinsuppToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoid = { neg := fun f => Dfinsupp.mapRange (fun x => Neg.neg) (_ : ∀ (x : ι), -0 = 0) f }
theorem Dfinsupp.neg_apply {ι : Type u} {β : ιType v} [inst : (i : ι) → AddGroup (β i)] (g : Dfinsupp fun i => β i) (i : ι) :
↑(-g) i = -g i
@[simp]
theorem Dfinsupp.coe_neg {ι : Type u} {β : ιType v} [inst : (i : ι) → AddGroup (β i)] (g : Dfinsupp fun i => β i) :
↑(-g) = -g
instance Dfinsupp.instSubDfinsuppToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoid {ι : Type u} {β : ιType v} [inst : (i : ι) → AddGroup (β i)] :
Sub (Dfinsupp fun i => β i)
Equations
• Dfinsupp.instSubDfinsuppToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoid = { sub := Dfinsupp.zipWith (fun x => Sub.sub) (_ : ∀ (x : ι), 0 - 0 = 0) }
theorem Dfinsupp.sub_apply {ι : Type u} {β : ιType v} [inst : (i : ι) → AddGroup (β i)] (g₁ : Dfinsupp fun i => β i) (g₂ : Dfinsupp fun i => β i) (i : ι) :
↑(g₁ - g₂) i = g₁ i - g₂ i
@[simp]
theorem Dfinsupp.coe_sub {ι : Type u} {β : ιType v} [inst : (i : ι) → AddGroup (β i)] (g₁ : Dfinsupp fun i => β i) (g₂ : Dfinsupp fun i => β i) :
↑(g₁ - g₂) = g₁ - g₂
instance Dfinsupp.hasIntScalar {ι : Type u} {β : ιType v} [inst : (i : ι) → AddGroup (β i)] :
SMul (Dfinsupp fun 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 => Dfinsupp.mapRange (fun x => (fun x_1 x_2 => x_1 x_2) c) (_ : ∀ (x : ι), c 0 = 0) v }
theorem Dfinsupp.zsmul_apply {ι : Type u} {β : ιType v} [inst : (i : ι) → AddGroup (β i)] (b : ) (v : Dfinsupp fun i => β i) (i : ι) :
↑(b v) i = b v i
@[simp]
theorem Dfinsupp.coe_zsmul {ι : Type u} {β : ιType v} [inst : (i : ι) → AddGroup (β i)] (b : ) (v : Dfinsupp fun i => β i) :
↑(b v) = b v
instance Dfinsupp.instAddGroupDfinsuppToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoid {ι : Type u} {β : ιType v} [inst : (i : ι) → AddGroup (β i)] :
AddGroup (Dfinsupp fun i => β i)
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
instance Dfinsupp.instSMulDfinsuppToZero {ι : Type u} {γ : Type w} {β : ιType v} [inst : ] [inst : (i : ι) → AddMonoid (β i)] [inst : (i : ι) → DistribMulAction γ (β i)] :
SMul γ (Dfinsupp fun i => β i)

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

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

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

Equations
• One or more equations did not get rendered due to their size.
instance Dfinsupp.module {ι : Type u} {γ : Type w} {β : ιType v} [inst : ] [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → Module γ (β i)] :
Module γ (Dfinsupp fun i => β i)

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

Equations
• One or more equations did not get rendered due to their size.
def Dfinsupp.filter {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] (p : ιProp) [inst : ] (x : Dfinsupp fun i => β i) :
Dfinsupp fun i => β i

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

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Dfinsupp.filter_apply {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] (p : ιProp) [inst : ] (i : ι) (f : Dfinsupp fun i => β i) :
↑() i = if p i then f i else 0
theorem Dfinsupp.filter_apply_pos {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] {p : ιProp} [inst : ] (f : Dfinsupp fun i => β i) {i : ι} (h : p i) :
↑() i = f i
theorem Dfinsupp.filter_apply_neg {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] {p : ιProp} [inst : ] (f : Dfinsupp fun i => β i) {i : ι} (h : ¬p i) :
↑() i = 0
theorem Dfinsupp.filter_pos_add_filter_neg {ι : Type u} {β : ιType v} [inst : (i : ι) → AddZeroClass (β i)] (f : Dfinsupp fun i => β i) (p : ιProp) [inst : ] :
+ Dfinsupp.filter (fun i => ¬p i) f = f
@[simp]
theorem Dfinsupp.filter_zero {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] (p : ιProp) [inst : ] :
= 0
@[simp]
theorem Dfinsupp.filter_add {ι : Type u} {β : ιType v} [inst : (i : ι) → AddZeroClass (β i)] (p : ιProp) [inst : ] (f : Dfinsupp fun i => β i) (g : Dfinsupp fun i => β i) :
Dfinsupp.filter p (f + g) = +
@[simp]
theorem Dfinsupp.filter_smul {ι : Type u} {γ : Type w} {β : ιType v} [inst : ] [inst : (i : ι) → AddMonoid (β i)] [inst : (i : ι) → DistribMulAction γ (β i)] (p : ιProp) [inst : ] (r : γ) (f : Dfinsupp fun i => β i) :
@[simp]
theorem Dfinsupp.filterAddMonoidHom_apply {ι : Type u} (β : ιType v) [inst : (i : ι) → AddZeroClass (β i)] (p : ιProp) [inst : ] (x : Dfinsupp fun i => β i) :
↑() x =
def Dfinsupp.filterAddMonoidHom {ι : Type u} (β : ιType v) [inst : (i : ι) → AddZeroClass (β i)] (p : ιProp) [inst : ] :
(Dfinsupp fun i => β i) →+ Dfinsupp fun i => β i

Dfinsupp.filter as an AddMonoidHom.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Dfinsupp.filterLinearMap_apply {ι : Type u} (γ : Type w) (β : ιType v) [inst : ] [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → Module γ (β i)] (p : ιProp) [inst : ] (x : Dfinsupp fun i => β i) :
↑() x =
def Dfinsupp.filterLinearMap {ι : Type u} (γ : Type w) (β : ιType v) [inst : ] [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → Module γ (β i)] (p : ιProp) [inst : ] :
(Dfinsupp fun i => β i) →ₗ[γ] Dfinsupp fun i => β i

Dfinsupp.filter as a LinearMap.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Dfinsupp.filter_neg {ι : Type u} {β : ιType v} [inst : (i : ι) → AddGroup (β i)] (p : ιProp) [inst : ] (f : Dfinsupp fun i => β i) :
@[simp]
theorem Dfinsupp.filter_sub {ι : Type u} {β : ιType v} [inst : (i : ι) → AddGroup (β i)] (p : ιProp) [inst : ] (f : Dfinsupp fun i => β i) (g : Dfinsupp fun i => β i) :
Dfinsupp.filter p (f - g) = -
def Dfinsupp.subtypeDomain {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] (p : ιProp) [inst : ] (x : Dfinsupp fun i => β i) :
Dfinsupp fun 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.
@[simp]
theorem Dfinsupp.subtypeDomain_zero {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] {p : ιProp} [inst : ] :
@[simp]
theorem Dfinsupp.subtypeDomain_apply {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] {p : ιProp} [inst : ] {i : } {v : Dfinsupp fun i => β i} :
↑() i = v i
@[simp]
theorem Dfinsupp.subtypeDomain_add {ι : Type u} {β : ιType v} [inst : (i : ι) → AddZeroClass (β i)] {p : ιProp} [inst : ] (v : Dfinsupp fun i => β i) (v' : Dfinsupp fun i => β i) :
@[simp]
theorem Dfinsupp.subtypeDomain_smul {ι : Type u} {γ : Type w} {β : ιType v} [inst : ] [inst : (i : ι) → AddMonoid (β i)] [inst : (i : ι) → DistribMulAction γ (β i)] {p : ιProp} [inst : ] (r : γ) (f : Dfinsupp fun i => β i) :
@[simp]
theorem Dfinsupp.subtypeDomainAddMonoidHom_apply {ι : Type u} (β : ιType v) [inst : (i : ι) → AddZeroClass (β i)] (p : ιProp) [inst : ] (x : Dfinsupp fun i => β i) :
def Dfinsupp.subtypeDomainAddMonoidHom {ι : Type u} (β : ιType v) [inst : (i : ι) → AddZeroClass (β i)] (p : ιProp) [inst : ] :
(Dfinsupp fun i => β i) →+ Dfinsupp fun i => β i

subtypeDomain but as an AddMonoidHom.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Dfinsupp.subtypeDomainLinearMap_apply {ι : Type u} (γ : Type w) (β : ιType v) [inst : ] [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → Module γ (β i)] (p : ιProp) [inst : ] (x : Dfinsupp fun i => β i) :
↑() x =
def Dfinsupp.subtypeDomainLinearMap {ι : Type u} (γ : Type w) (β : ιType v) [inst : ] [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → Module γ (β i)] (p : ιProp) [inst : ] :
(Dfinsupp fun i => β i) →ₗ[γ] Dfinsupp fun i => β i

Dfinsupp.subtypeDomain as a LinearMap.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Dfinsupp.subtypeDomain_neg {ι : Type u} {β : ιType v} [inst : (i : ι) → AddGroup (β i)] {p : ιProp} [inst : ] {v : Dfinsupp fun i => β i} :
@[simp]
theorem Dfinsupp.subtypeDomain_sub {ι : Type u} {β : ιType v} [inst : (i : ι) → AddGroup (β i)] {p : ιProp} [inst : ] {v : Dfinsupp fun i => β i} {v' : Dfinsupp fun i => β i} :
theorem Dfinsupp.finite_support {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] (f : Dfinsupp fun i => β i) :
Set.Finite { i | f i 0 }
def Dfinsupp.mk {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] (s : ) (x : (i : s) → β i) :
Dfinsupp fun i => β i

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

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Dfinsupp.mk_apply {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] {s : } {x : (i : s) → β i} {i : ι} :
↑() i = if H : i s then x { val := i, property := H } else 0
theorem Dfinsupp.mk_of_mem {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] {s : } {x : (i : s) → β i} {i : ι} (hi : i s) :
↑() i = x { val := i, property := hi }
theorem Dfinsupp.mk_of_not_mem {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] {s : } {x : (i : s) → β i} {i : ι} (hi : ¬i s) :
↑() i = 0
theorem Dfinsupp.mk_injective {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] (s : ) :
instance Dfinsupp.unique {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] [inst : ∀ (i : ι), Subsingleton (β i)] :
Unique (Dfinsupp fun i => β i)
Equations
instance Dfinsupp.uniqueOfIsEmpty {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] [inst : ] :
Unique (Dfinsupp fun i => β i)
Equations
@[simp]
theorem Dfinsupp.equivFunOnFintype_apply {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] [inst : ] :
∀ (a : Dfinsupp fun i => (fun i => β i) i) (a_1 : ι), Dfinsupp.equivFunOnFintype a a_1 = a a_1
def Dfinsupp.equivFunOnFintype {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] [inst : ] :
(Dfinsupp fun 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
• One or more equations did not get rendered due to their size.
@[simp]
theorem Dfinsupp.equivFunOnFintype_symm_coe {ι : Type u} {β : ιType v} [inst : (i : ι) → Zero (β i)] [inst : ] (f : Dfinsupp fun i => β i) :
↑(Equiv.symm Dfinsupp.equivFunOnFintype) f = f
def Dfinsupp.single {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] (i : ι) (b : β i) :
Dfinsupp fun 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 : ] [inst : (i : ι) → Zero (β i)] {i : ι} {b : β i} :
↑() =
@[simp]
theorem Dfinsupp.single_apply {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] {i : ι} {i' : ι} {b : β i} :
↑() i' = if h : i = i' then Eq.recOn h b else 0
@[simp]
theorem Dfinsupp.single_zero {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] (i : ι) :
= 0
theorem Dfinsupp.single_eq_same {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] {i : ι} {b : β i} :
↑() i = b
theorem Dfinsupp.single_eq_of_ne {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] {i : ι} {i' : ι} {b : β i} (h : i i') :
↑() i' = 0
theorem Dfinsupp.single_injective {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] {i : ι} :
theorem Dfinsupp.single_eq_single_iff {ι : Type u} {β : ιType v} [dec : ] [inst : (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} [dec : ] [inst : (i : ι) → Zero (β i)] {b : (i : ι) → β i} (h : ∀ (i : ι), b i 0) :

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 : ] [inst : (i : ι) → Zero (β i)] {i : ι} {xi : β i} :
= 0 xi = 0
theorem Dfinsupp.filter_single {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] (p : ιProp) [inst : ] (i : ι) (x : β i) :
= if p i then else 0
@[simp]
theorem Dfinsupp.filter_single_pos {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] {p : ιProp} [inst : ] (i : ι) (x : β i) (h : p i) :
=
@[simp]
theorem Dfinsupp.filter_single_neg {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] {p : ιProp} [inst : ] (i : ι) (x : β i) (h : ¬p i) :
= 0
theorem Dfinsupp.single_eq_of_sigma_eq {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] {i : ι} {j : ι} {xi : β i} {xj : β j} (h : { fst := i, snd := xi } = { fst := j, snd := xj }) :
=

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

@[simp]
theorem Dfinsupp.equivFunOnFintype_single {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : ] (i : ι) (m : β i) :
Dfinsupp.equivFunOnFintype () =
@[simp]
theorem Dfinsupp.equivFunOnFintype_symm_single {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : ] (i : ι) (m : β i) :
↑(Equiv.symm Dfinsupp.equivFunOnFintype) () =
def Dfinsupp.erase {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] (i : ι) (x : Dfinsupp fun i => β i) :
Dfinsupp fun i => β i

Redefine f i to be 0.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Dfinsupp.erase_apply {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] {i : ι} {j : ι} {f : Dfinsupp fun i => β i} :
↑() j = if j = i then 0 else f j
theorem Dfinsupp.erase_same {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] {i : ι} {f : Dfinsupp fun i => β i} :
↑() i = 0
theorem Dfinsupp.erase_ne {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] {i : ι} {i' : ι} {f : Dfinsupp fun i => β i} (h : i' i) :
↑() i' = f i'
theorem Dfinsupp.piecewise_single_erase {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] (x : Dfinsupp fun i => β i) (i : ι) [inst : (i' : ι) → Decidable (i' {i})] :
Dfinsupp.piecewise (Dfinsupp.single i (x i)) () {i} = x
theorem Dfinsupp.erase_eq_sub_single {ι : Type u} [dec : ] {β : ιType u_1} [inst : (i : ι) → AddGroup (β i)] (f : Dfinsupp fun i => β i) (i : ι) :
= f - Dfinsupp.single i (f i)
@[simp]
theorem Dfinsupp.erase_zero {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] (i : ι) :
= 0
@[simp]
theorem Dfinsupp.filter_ne_eq_erase {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] (f : Dfinsupp fun i => β i) (i : ι) :
Dfinsupp.filter (fun x => x i) f =
@[simp]
theorem Dfinsupp.filter_ne_eq_erase' {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] (f : Dfinsupp fun i => β i) (i : ι) :
Dfinsupp.filter ((fun x x_1 => x x_1) i) f =
theorem Dfinsupp.erase_single {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] (j : ι) (i : ι) (x : β i) :
= if i = j then 0 else
@[simp]
theorem Dfinsupp.erase_single_same {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] (i : ι) (x : β i) :
= 0
@[simp]
theorem Dfinsupp.erase_single_ne {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] {i : ι} {j : ι} (x : β i) (h : i j) :
=
def Dfinsupp.update {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] (i : ι) (f : Dfinsupp fun i => β i) (b : β i) :
Dfinsupp fun 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
• One or more equations did not get rendered due to their size.
@[simp]
theorem Dfinsupp.coe_update {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] (i : ι) (f : Dfinsupp fun i => β i) (b : β i) :
↑() = Function.update (f) i b
@[simp]
theorem Dfinsupp.update_self {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] (i : ι) (f : Dfinsupp fun i => β i) :
Dfinsupp.update i f (f i) = f
@[simp]
theorem Dfinsupp.update_eq_erase {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] (i : ι) (f : Dfinsupp fun i => β i) :
=
theorem Dfinsupp.update_eq_single_add_erase {ι : Type u} [dec : ] {β : ιType u_1} [inst : (i : ι) → AddZeroClass (β i)] (f : Dfinsupp fun i => β i) (i : ι) (b : β i) :
= +
theorem Dfinsupp.update_eq_erase_add_single {ι : Type u} [dec : ] {β : ιType u_1} [inst : (i : ι) → AddZeroClass (β i)] (f : Dfinsupp fun i => β i) (i : ι) (b : β i) :
= +
theorem Dfinsupp.update_eq_sub_add_single {ι : Type u} [dec : ] {β : ιType u_1} [inst : (i : ι) → AddGroup (β i)] (f : Dfinsupp fun i => β i) (i : ι) (b : β i) :
= f - Dfinsupp.single i (f i) +
@[simp]
theorem Dfinsupp.single_add {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] (i : ι) (b₁ : β i) (b₂ : β i) :
Dfinsupp.single i (b₁ + b₂) = +
@[simp]
theorem Dfinsupp.erase_add {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] (i : ι) (f₁ : Dfinsupp fun i => β i) (f₂ : Dfinsupp fun i => β i) :
Dfinsupp.erase i (f₁ + f₂) = +
@[simp]
theorem Dfinsupp.singleAddHom_apply {ι : Type u} (β : ιType v) [dec : ] [inst : (i : ι) → AddZeroClass (β i)] (i : ι) (b : β i) :
↑() b =
def Dfinsupp.singleAddHom {ι : Type u} (β : ιType v) [dec : ] [inst : (i : ι) → AddZeroClass (β i)] (i : ι) :
β i →+ Dfinsupp fun i => β i

Dfinsupp.single as an AddMonoidHom.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Dfinsupp.eraseAddHom_apply {ι : Type u} (β : ιType v) [dec : ] [inst : (i : ι) → AddZeroClass (β i)] (i : ι) (x : Dfinsupp fun i => β i) :
↑() x =
def Dfinsupp.eraseAddHom {ι : Type u} (β : ιType v) [dec : ] [inst : (i : ι) → AddZeroClass (β i)] (i : ι) :
(Dfinsupp fun i => β i) →+ Dfinsupp fun i => β i

Dfinsupp.erase as an AddMonoidHom.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Dfinsupp.single_neg {ι : Type u} [dec : ] {β : ιType v} [inst : (i : ι) → AddGroup (β i)] (i : ι) (x : β i) :
@[simp]
theorem Dfinsupp.single_sub {ι : Type u} [dec : ] {β : ιType v} [inst : (i : ι) → AddGroup (β i)] (i : ι) (x : β i) (y : β i) :
Dfinsupp.single i (x - y) = -
@[simp]
theorem Dfinsupp.erase_neg {ι : Type u} [dec : ] {β : ιType v} [inst : (i : ι) → AddGroup (β i)] (i : ι) (f : Dfinsupp fun i => β i) :
@[simp]
theorem Dfinsupp.erase_sub {ι : Type u} [dec : ] {β : ιType v} [inst : (i : ι) → AddGroup (β i)] (i : ι) (f : Dfinsupp fun i => β i) (g : Dfinsupp fun i => β i) :
Dfinsupp.erase i (f - g) = -
theorem Dfinsupp.single_add_erase {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] (i : ι) (f : Dfinsupp fun i => β i) :
Dfinsupp.single i (f i) + = f
theorem Dfinsupp.erase_add_single {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] (i : ι) (f : Dfinsupp fun i => β i) :
+ Dfinsupp.single i (f i) = f
theorem Dfinsupp.induction {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] {p : (Dfinsupp fun i => β i) → Prop} (f : Dfinsupp fun i => β i) (h0 : p 0) (ha : (i : ι) → (b : β i) → (f : Dfinsupp fun i => β i) → f i = 0b 0p fp ( + f)) :
p f
theorem Dfinsupp.induction₂ {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] {p : (Dfinsupp fun i => β i) → Prop} (f : Dfinsupp fun i => β i) (h0 : p 0) (ha : (i : ι) → (b : β i) → (f : Dfinsupp fun i => β i) → f i = 0b 0p fp (f + )) :
p f
@[simp]
theorem Dfinsupp.add_closure_unionᵢ_range_single {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] :
theorem Dfinsupp.addHom_ext {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] {γ : Type w} [inst : ] ⦃f : (Dfinsupp fun i => β i) →+ γ ⦃g : (Dfinsupp fun i => β i) →+ γ (H : ∀ (i : ι) (y : β i), f () = g ()) :
f = g

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

theorem Dfinsupp.addHom_ext' {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] {γ : Type w} [inst : ] ⦃f : (Dfinsupp fun i => β i) →+ γ ⦃g : (Dfinsupp fun i => β i) →+ γ (H : ∀ (x : ι), ) :
f = g

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

See note [partially-applied ext lemmas].

@[simp]
theorem Dfinsupp.mk_add {ι : Type u} {β : ιType v} [dec : ] [inst : (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} [dec : ] [inst : (i : ι) → Zero (β i)] {s : } :
= 0
@[simp]
theorem Dfinsupp.mk_neg {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → AddGroup (β i)] {s : } {x : (i : s) → β i} :
@[simp]
theorem Dfinsupp.mk_sub {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → AddGroup (β i)] {s : } {x : (i : s) → β i} {y : (i : s) → β i} :
Dfinsupp.mk s (x - y) = -
def Dfinsupp.mkAddGroupHom {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → AddGroup (β i)] (s : ) :
((i : s) → β i) →+ Dfinsupp fun 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
• One or more equations did not get rendered due to their size.
@[simp]
theorem Dfinsupp.mk_smul {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : ] [inst : (i : ι) → AddMonoid (β i)] [inst : (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} [dec : ] [inst : ] [inst : (i : ι) → AddMonoid (β i)] [inst : (i : ι) → DistribMulAction γ (β i)] {i : ι} (c : γ) (x : β i) :
def Dfinsupp.support {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] (f : Dfinsupp fun i => β i) :

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

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Dfinsupp.support_mk_subset {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] {s : } {x : (i : s) → β i} :
s
@[simp]
theorem Dfinsupp.support_mk'_subset {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] {f : (i : ι) → β i} {s : } {h : ∀ (i : ι), i s f i = 0} :
Dfinsupp.support { toFun := f, support' := Trunc.mk { val := s, property := h } }
@[simp]
theorem Dfinsupp.mem_support_toFun {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] (f : Dfinsupp fun i => β i) (i : ι) :
f i 0
theorem Dfinsupp.eq_mk_support {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] (f : Dfinsupp fun i => β i) :
f = Dfinsupp.mk () fun i => f i
@[simp]
theorem Dfinsupp.support_zero {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] :
theorem Dfinsupp.mem_support_iff {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] {f : Dfinsupp fun i => β i} {i : ι} :
f i 0
theorem Dfinsupp.not_mem_support_iff {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] {f : Dfinsupp fun i => β i} {i : ι} :
¬ f i = 0
@[simp]
theorem Dfinsupp.support_eq_empty {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] {f : Dfinsupp fun i => β i} :
f = 0
instance Dfinsupp.decidableZero {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] :
Equations
theorem Dfinsupp.support_subset_iff {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] {s : Set ι} {f : Dfinsupp fun i => β i} :
↑() s ∀ (i : ι), ¬i sf i = 0
theorem Dfinsupp.support_single_ne_zero {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] {i : ι} {b : β i} (hb : b 0) :
= {i}
theorem Dfinsupp.support_single_subset {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] {i : ι} {b : β i} :
{i}
theorem Dfinsupp.mapRange_def {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [dec : ] [inst : (i : ι) → Zero (β₁ i)] [inst : (i : ι) → Zero (β₂ i)] [inst : (i : ι) → (x : β₁ i) → Decidable (x 0)] {f : (i : ι) → β₁ iβ₂ i} {hf : ∀ (i : ι), f i 0 = 0} {g : Dfinsupp fun i => β₁ i} :
= Dfinsupp.mk () fun i => f (i) (g i)
@[simp]
theorem Dfinsupp.mapRange_single {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [dec : ] [inst : (i : ι) → Zero (β₁ i)] [inst : (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₂} [dec : ] [inst : (i : ι) → Zero (β₁ i)] [inst : (i : ι) → Zero (β₂ i)] [inst : (i : ι) → (x : β₁ i) → Decidable (x 0)] [inst : (i : ι) → (x : β₂ i) → Decidable (x 0)] {f : (i : ι) → β₁ iβ₂ i} {hf : ∀ (i : ι), f i 0 = 0} {g : Dfinsupp fun i => β₁ i} :
theorem Dfinsupp.zipWith_def {ι : Type u} {β : ιType v} {β₁ : ιType v₁} {β₂ : ιType v₂} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → Zero (β₁ i)] [inst : (i : ι) → Zero (β₂ i)] [inst : (i : ι) → (x : β₁ i) → Decidable (x 0)] [inst : (i : ι) → (x : β₂ i) → Decidable (x 0)] {f : (i : ι) → β₁ iβ₂ iβ i} {hf : ∀ (i : ι), f i 0 0 = 0} {g₁ : Dfinsupp fun i => β₁ i} {g₂ : Dfinsupp fun i => β₂ i} :
Dfinsupp.zipWith f hf g₁ g₂ = Dfinsupp.mk () fun i => f (i) (g₁ i) (g₂ i)
theorem Dfinsupp.support_zipWith {ι : Type u} {β : ιType v} {β₁ : ιType v₁} {β₂ : ιType v₂} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : (i : ι) → Zero (β₁ i)] [inst : (i : ι) → Zero (β₂ i)] [inst : (i : ι) → (x : β₁ i) → Decidable (x 0)] [inst : (i : ι) → (x : β₂ i) → Decidable (x 0)] {f : (i : ι) → β₁ iβ₂ iβ i} {hf : ∀ (i : ι), f i 0 0 = 0} {g₁ : Dfinsupp fun i => β₁ i} {g₂ : Dfinsupp fun i => β₂ i} :
theorem Dfinsupp.erase_def {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] (i : ι) (f : Dfinsupp fun i => β i) :
= Dfinsupp.mk () fun j => f j
@[simp]
theorem Dfinsupp.support_erase {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] (i : ι) (f : Dfinsupp fun i => β i) :
theorem Dfinsupp.support_update_ne_zero {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] (f : Dfinsupp fun i => β i) (i : ι) {b : β i} (h : b 0) :
theorem Dfinsupp.support_update {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] (f : Dfinsupp fun i => β i) (i : ι) (b : β i) [inst : Decidable (b = 0)] :
Dfinsupp.support () = if b = 0 then else
theorem Dfinsupp.filter_def {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] {p : ιProp} [inst : ] (f : Dfinsupp fun i => β i) :
= Dfinsupp.mk () fun i => f i
@[simp]
theorem Dfinsupp.support_filter {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] {p : ιProp} [inst : ] (f : Dfinsupp fun i => β i) :
theorem Dfinsupp.subtypeDomain_def {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] {p : ιProp} [inst : ] (f : Dfinsupp fun i => β i) :
= Dfinsupp.mk () fun i => f i
@[simp]
theorem Dfinsupp.support_subtypeDomain {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] {p : ιProp} [inst : ] {f : Dfinsupp fun i => β i} :
theorem Dfinsupp.support_add {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] {g₁ : Dfinsupp fun i => β i} {g₂ : Dfinsupp fun i => β i} :
Dfinsupp.support (g₁ + g₂)
@[simp]
theorem Dfinsupp.support_neg {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → AddGroup (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] {f : Dfinsupp fun i => β i} :
theorem Dfinsupp.support_smul {ι : Type u} {β : ιType v} [dec : ] {γ : Type w} [inst : ] [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → Module γ (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] (b : γ) (v : Dfinsupp fun i => β i) :
instance Dfinsupp.instDecidableEqDfinsupp {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → DecidableEq (β i)] :
DecidableEq (Dfinsupp fun i => β i)
Equations
• One or more equations did not get rendered due to their size.
noncomputable def Dfinsupp.comapDomain {ι : Type u} {β : ιType v} [dec : ] {κ : Type u_1} [inst : (i : ι) → Zero (β i)] (h : κι) (hh : ) (f : Dfinsupp fun i => β i) :
Dfinsupp fun k => β (h k)

Reindexing (and possibly removing) terms of a dfinsupp.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Dfinsupp.comapDomain_apply {ι : Type u} {β : ιType v} [dec : ] {κ : Type u_1} [inst : (i : ι) → Zero (β i)] (h : κι) (hh : ) (f : Dfinsupp fun i => β i) (k : κ) :
↑() k = f (h k)
@[simp]
theorem Dfinsupp.comapDomain_zero {ι : Type u} {β : ιType v} [dec : ] {κ : Type u_1} [inst : (i : ι) → Zero (β i)] (h : κι) (hh : ) :
= 0
@[simp]
theorem Dfinsupp.comapDomain_add {ι : Type u} {β : ιType v} [dec : ] {κ : Type u_1} [inst : (i : ι) → AddZeroClass (β i)] (h : κι) (hh : ) (f : Dfinsupp fun i => β i) (g : Dfinsupp fun i => β i) :
@[simp]
theorem Dfinsupp.comapDomain_smul {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] {κ : Type u_1} [inst : ] [inst : (i : ι) → AddMonoid (β i)] [inst : (i : ι) → DistribMulAction γ (β i)] (h : κι) (hh : ) (r : γ) (f : Dfinsupp fun i => β i) :
@[simp]
theorem Dfinsupp.comapDomain_single {ι : Type u} {β : ιType v} [dec : ] {κ : Type u_1} [inst : ] [inst : (i : ι) → Zero (β i)] (h : κι) (hh : ) (k : κ) (x : β (h k)) :
def Dfinsupp.comapDomain' {ι : Type u} {β : ιType v} {κ : Type u_1} [inst : (i : ι) → Zero (β i)] (h : κι) {h' : ικ} (hh' : ) (f : Dfinsupp fun i => β i) :
Dfinsupp fun 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.
@[simp]
theorem Dfinsupp.comapDomain'_apply {ι : Type u} {β : ιType v} {κ : Type u_1} [inst : (i : ι) → Zero (β i)] (h : κι) {h' : ικ} (hh' : ) (f : Dfinsupp fun i => β i) (k : κ) :
↑() k = f (h k)
@[simp]
theorem Dfinsupp.comapDomain'_zero {ι : Type u} {β : ιType v} {κ : Type u_1} [inst : (i : ι) → Zero (β i)] (h : κι) {h' : ικ} (hh' : ) :
= 0
@[simp]
theorem Dfinsupp.comapDomain'_add {ι : Type u} {β : ιType v} {κ : Type u_1} [inst : (i : ι) → AddZeroClass (β i)] (h : κι) {h' : ικ} (hh' : ) (f : Dfinsupp fun i => β i) (g : Dfinsupp fun i => β i) :
Dfinsupp.comapDomain' h hh' (f + g) = +
@[simp]
theorem Dfinsupp.comapDomain'_smul {ι : Type u} {γ : Type w} {β : ιType v} {κ : Type u_1} [inst : ] [inst : (i : ι) → AddMonoid (β i)] [inst : (i : ι) → DistribMulAction γ (β i)] (h : κι) {h' : ικ} (hh' : ) (r : γ) (f : Dfinsupp fun i => β i) :
@[simp]
theorem Dfinsupp.comapDomain'_single {ι : Type u} {β : ιType v} {κ : Type u_1} [inst : ] [inst : ] [inst : (i : ι) → Zero (β i)] (h : κι) {h' : ικ} (hh' : ) (k : κ) (x : β (h k)) :
@[simp]
theorem Dfinsupp.equivCongrLeft_apply {ι : Type u} {β : ιType v} {κ : Type u_1} [inst : (i : ι) → Zero (β i)] (h : ι κ) (f : Dfinsupp fun i => β i) :
↑() f = Dfinsupp.comapDomain' ↑() (_ : Function.RightInverse h.invFun h.toFun) f
def Dfinsupp.equivCongrLeft {ι : Type u} {β : ιType v} {κ : Type u_1} [inst : (i : ι) → Zero (β i)] (h : ι κ) :
(Dfinsupp fun i => β i) Dfinsupp fun k => β (↑() 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.
instance Dfinsupp.hasAdd₂ {ι : Type u} {α : ιType u_1} {δ : (i : ι) → α iType v} [inst : (i : ι) → (j : α i) → AddZeroClass (δ i j)] :
Add (Dfinsupp fun i => Dfinsupp fun j => δ i j)
Equations
instance Dfinsupp.addZeroClass₂ {ι : Type u} {α : ιType u_1} {δ : (i : ι) → α iType v} [inst : (i : ι) → (j : α i) → AddZeroClass (δ i j)] :
AddZeroClass (Dfinsupp fun i => Dfinsupp fun j => δ i j)
Equations
instance Dfinsupp.addMonoid₂ {ι : Type u} {α : ιType u_1} {δ : (i : ι) → α iType v} [inst : (i : ι) → (j : α i) → AddMonoid (δ i j)] :
AddMonoid (Dfinsupp fun i => Dfinsupp fun j => δ i j)
Equations
instance Dfinsupp.distribMulAction₂ {ι : Type u} {γ : Type w} {α : ιType u_1} {δ : (i : ι) → α iType v} [inst : ] [inst : (i : ι) → (j : α i) → AddMonoid (δ i j)] [inst : (i : ι) → (j : α i) → DistribMulAction γ (δ i j)] :
DistribMulAction γ (Dfinsupp fun i => Dfinsupp fun j => δ i j)
Equations
• Dfinsupp.distribMulAction₂ = Dfinsupp.distribMulAction
noncomputable def Dfinsupp.sigmaCurry {ι : Type u} {α : ιType u_1} {δ : (i : ι) → α iType v} [inst : (i : ι) → (j : α i) → Zero (δ i j)] (f : Dfinsupp fun i => δ i.fst i.snd) :
Dfinsupp fun i => Dfinsupp fun j => δ 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.
@[simp]
theorem Dfinsupp.sigmaCurry_apply {ι : Type u} {α : ιType u_1} {δ : (i : ι) → α iType v} [inst : (i : ι) → (j : α i) → Zero (δ i j)] (f : Dfinsupp fun i => δ i.fst i.snd) (i : ι) (j : α i) :
↑(↑() i) j = f { fst := i, snd := j }
@[simp]
theorem Dfinsupp.sigmaCurry_zero {ι : Type u} {α : ιType u_1} {δ : (i : ι) → α iType v} [inst : (i : ι) → (j : α i) → Zero (δ i j)] :
@[simp]
theorem Dfinsupp.sigmaCurry_add {ι : Type u} {α : ιType u_1} {δ : (i : ι) → α iType v} [inst : (i : ι) → (j : α i) → AddZeroClass (δ i j)] (f : Dfinsupp fun i => δ i.fst i.snd) (g : Dfinsupp fun i => δ i.fst i.snd) :
@[simp]
theorem Dfinsupp.sigmaCurry_smul {ι : Type u} {γ : Type w} {α : ιType u_1} {δ : (i : ι) → α iType v} [inst : ] [inst : (i : ι) → (j : α i) → AddMonoid (δ i j)] [inst : (i : ι) → (j : α i) → DistribMulAction γ (δ i j)] (r : γ) (f : Dfinsupp fun i => δ i.fst i.snd) :
@[simp]
theorem Dfinsupp.sigmaCurry_single {ι : Type u} [dec : ] {α : ιType u_1} {δ : (i : ι) → α iType v} [inst : (i : ι) → DecidableEq (α i)] [inst : (i : ι) → (j : α i) → Zero (δ i j)] (ij : (i : ι) × α i) (x : δ ij.fst ij.snd) :
= Dfinsupp.single ij.fst (Dfinsupp.single ij.snd x)
noncomputable def Dfinsupp.sigmaUncurry {ι : Type u} {α : ιType u_1} {δ : (i : ι) → α iType v} [inst : (i : ι) → (j : α i) → Zero (δ i j)] [inst : (i : ι) → DecidableEq (α i)] [inst : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x 0)] (f : Dfinsupp fun i => Dfinsupp fun j => δ i j) :
Dfinsupp fun 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.
@[simp]
theorem Dfinsupp.sigmaUncurry_apply {ι : Type u} {α : ιType u_1} {δ : (i : ι) → α iType v} [inst : (i : ι) → (j : α i) → Zero (δ i j)] [inst : (i : ι) → DecidableEq (α i)] [inst : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x 0)] (f : Dfinsupp fun i => Dfinsupp fun j => δ i j) (i : ι) (j : α i) :
↑() { fst := i, snd := j } = ↑(f i) j
@[simp]
theorem Dfinsupp.sigmaUncurry_zero {ι : Type u} {α : ιType u_1} {δ : (i : ι) → α iType v} [inst : (i : ι) → (j : α i) → Zero (δ i j)] [inst : (i : ι) → DecidableEq (α i)] [inst : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x 0)] :
@[simp]
theorem Dfinsupp.sigmaUncurry_add {ι : Type u} {α : ιType u_1} {δ : (i : ι) → α iType v} [inst : (i : ι) → (j : α i) → AddZeroClass (δ i j)] [inst : (i : ι) → DecidableEq (α i)] [inst : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x 0)] (f : Dfinsupp fun i => Dfinsupp fun j => δ i j) (g : Dfinsupp fun i => Dfinsupp fun j => δ i j) :
@[simp]
theorem Dfinsupp.sigmaUncurry_smul {ι : Type u} {γ : Type w} {α : ιType u_1} {δ : (i : ι) → α iType v} [inst : ] [inst : (i : ι) → (j : α i) → AddMonoid (δ i j)] [inst : (i : ι) → DecidableEq (α i)] [inst : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x 0)] [inst : (i : ι) → (j : α i) → DistribMulAction γ (δ i j)] (r : γ) (f : Dfinsupp fun i => Dfinsupp fun j => δ i j) :
@[simp]
theorem Dfinsupp.sigmaUncurry_single {ι : Type u} [dec : ] {α : ιType u_1} {δ : (i : ι) → α iType v} [inst : (i : ι) → (j : α i) → Zero (δ i j)] [inst : (i : ι) → DecidableEq (α i)] [inst : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x 0)] (i : ι) (j : α i) (x : δ i j) :
= Dfinsupp.single { fst := i, snd := j } x
noncomputable def Dfinsupp.sigmaCurryEquiv {ι : Type u} {α : ιType u_1} {δ : (i : ι) → α iType v} [inst : (i : ι) → (j : α i) → Zero (δ i j)] [inst : (i : ι) → DecidableEq (α i)] [inst : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x 0)] :
(Dfinsupp fun i => δ i.fst i.snd) Dfinsupp fun i => Dfinsupp fun j => δ 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
• One or more equations did not get rendered due to their size.
def Dfinsupp.extendWith {ι : Type u} {α : Type v} [inst : (i : ) → Zero (α i)] (a : α none) (f : Dfinsupp fun i => α (some i)) :
Dfinsupp fun 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.
@[simp]
theorem Dfinsupp.extendWith_none {ι : Type u} {α : Type v} [inst : (i : ) → Zero (α i)] (f : Dfinsupp fun i => α (some i)) (a : α none) :
↑() none = a
@[simp]
theorem Dfinsupp.extendWith_some {ι : Type u} {α : Type v} [inst : (i : ) → Zero (α i)] (f : Dfinsupp fun i => α (some i)) (a : α none) (i : ι) :
↑() (some i) = f i
@[simp]
theorem Dfinsupp.extendWith_single_zero {ι : Type u} {α : Type v} [inst : ] [inst : (i : ) → Zero (α i)] (i : ι) (x : α (some i)) :
@[simp]
theorem Dfinsupp.extendWith_zero {ι : Type u} {α : Type v} [inst : ] [inst : (i : ) → Zero (α i)] (x : α none) :
@[simp]
theorem Dfinsupp.equivProdDfinsupp_apply {ι : Type u} [dec : ] {α : Type v} [inst : (i : ) → Zero (α i)] (f : Dfinsupp fun i => α i) :
Dfinsupp.equivProdDfinsupp f = (f none, Dfinsupp.comapDomain some (_ : ) f)
@[simp]
theorem Dfinsupp.equivProdDfinsupp_symm_apply {ι : Type u} [dec : ] {α : Type v} [inst : (i : ) → Zero (α i)] (f : α none × Dfinsupp fun i => α (some i)) :
↑(Equiv.symm Dfinsupp.equivProdDfinsupp) f = Dfinsupp.extendWith f.fst f.snd
noncomputable def Dfinsupp.equivProdDfinsupp {ι : Type u} [dec : ] {α : Type v} [inst : (i : ) → Zero (α i)] :
(Dfinsupp fun i => α i) α none × Dfinsupp fun 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.
theorem Dfinsupp.equivProdDfinsupp_add {ι : Type u} [dec : ] {α : Type v} [inst : (i : ) → AddZeroClass (α i)] (f : Dfinsupp fun i => α i) (g : Dfinsupp fun i => α i) :
Dfinsupp.equivProdDfinsupp (f + g) = Dfinsupp.equivProdDfinsupp f + Dfinsupp.equivProdDfinsupp g
theorem Dfinsupp.equivProdDfinsupp_smul {ι : Type u} {γ : Type w} [dec : ] {α : Type v} [inst : ] [inst : (i : ) → AddMonoid (α i)] [inst : (i : ) → DistribMulAction γ (α i)] (r : γ) (f : Dfinsupp fun i => α i) :
Dfinsupp.equivProdDfinsupp (r f) = r Dfinsupp.equivProdDfinsupp f
def Dfinsupp.sum {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] (f : Dfinsupp fun i => β i) (g : (i : ι) → β iγ) :
γ

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

Equations
def Dfinsupp.prod {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] (f : Dfinsupp fun i => β i) (g : (i : ι) → β iγ) :
γ

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

Equations
theorem Dfinsupp.sum_mapRange_index {ι : Type u} {γ : Type w} [dec : ] {β₁ : ιType v₁} {β₂ : ιType v₂} [inst : (i : ι) → Zero (β₁ i)] [inst : (i : ι) → Zero (β₂ i)] [inst : (i : ι) → (x : β₁ i) → Decidable (x 0)] [inst : (i : ι) → (x : β₂ i) → Decidable (x 0)] [inst : ] {f : (i : ι) → β₁ iβ₂ i} {hf : ∀ (i : ι), f i 0 = 0} {g : Dfinsupp fun i => β₁ i} {h : (i : ι) → β₂ iγ} (h0 : ∀ (i : ι), h i 0 = 0) :
Dfinsupp.sum () h = Dfinsupp.sum g fun i b => h i (f i b)
theorem Dfinsupp.prod_mapRange_index {ι : Type u} {γ : Type w} [dec : ] {β₁ : ιType v₁} {β₂ : ιType v₂} [inst : (i : ι) → Zero (β₁ i)] [inst : (i : ι) → Zero (β₂ i)] [inst : (i : ι) → (x : β₁ i) → Decidable (x 0)] [inst : (i : ι) → (x : β₂ i) → Decidable (x 0)] [inst : ] {f : (i : ι) → β₁ iβ₂ i} {hf : ∀ (i : ι), f i 0 = 0} {g : Dfinsupp fun i => β₁ i} {h : (i : ι) → β₂ iγ} (h0 : ∀ (i : ι), h i 0 = 1) :
Dfinsupp.prod () h = Dfinsupp.prod g fun i b => h i (f i b)
theorem Dfinsupp.sum_zero_index {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {h : (i : ι) → β iγ} :
= 0
theorem Dfinsupp.prod_zero_index {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {h : (i : ι) → β iγ} :
= 1
theorem Dfinsupp.sum_single_index {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {i : ι} {b : β i} {h : (i : ι) → β iγ} (h_zero : h i 0 = 0) :
Dfinsupp.sum () h = h i b
theorem Dfinsupp.prod_single_index {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {i : ι} {b : β i} {h : (i : ι) → β iγ} (h_zero : h i 0 = 1) :
Dfinsupp.prod () h = h i b
theorem Dfinsupp.sum_neg_index {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddGroup (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {g : Dfinsupp fun i => β i} {h : (i : ι) → β iγ} (h0 : ∀ (i : ι), h i 0 = 0) :
Dfinsupp.sum (-g) h = Dfinsupp.sum g fun i b => h i (-b)
theorem Dfinsupp.prod_neg_index {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddGroup (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {g : Dfinsupp fun i => β i} {h : (i : ι) → β iγ} (h0 : ∀ (i : ι), h i 0 = 1) :
Dfinsupp.prod (-g) h = Dfinsupp.prod g fun i b => h i (-b)
theorem Dfinsupp.sum_comm {γ : Type w} {ι₁ : Type u_1} {ι₂ : Type u_2} {β₁ : ι₁Type u_3} {β₂ : ι₂Type u_4} [inst : ] [inst : ] [inst : (i : ι₁) → Zero (β₁ i)] [inst : (i : ι₂) → Zero (β₂ i)] [inst : (i : ι₁) → (x : β₁ i) → Decidable (x 0)] [inst : (i : ι₂) → (x : β₂ i) → Decidable (x 0)] [inst : ] (f₁ : Dfinsupp fun i => β₁ i) (f₂ : Dfinsupp fun i => β₂ i) (h : (i : ι₁) → β₁ i(i : ι₂) → β₂ iγ) :
(Dfinsupp.sum f₁ fun i₁ x₁ => Dfinsupp.sum f₂ fun i₂ x₂ => h i₁ x₁ i₂ x₂) = Dfinsupp.sum f₂ fun i₂ x₂ => Dfinsupp.sum f₁ fun i₁ x₁ => h i₁ x₁ i₂ x₂
theorem Dfinsupp.prod_comm {γ : Type w} {ι₁ : Type u_1} {ι₂ : Type u_2} {β₁ : ι₁Type u_3} {β₂ : ι₂Type u_4} [inst : ] [inst : ] [inst : (i : ι₁) → Zero (β₁ i)] [inst : (i : ι₂) → Zero (β₂ i)] [inst : (i : ι₁) → (x : β₁ i) → Decidable (x 0)] [inst : (i : ι₂) → (x : β₂ i) → Decidable (x 0)] [inst : ] (f₁ : Dfinsupp fun i => β₁ i) (f₂ : Dfinsupp fun i => β₂ i) (h : (i : ι₁) → β₁ i(i : ι₂) → β₂ iγ) :
(Dfinsupp.prod f₁ fun i₁ x₁ => Dfinsupp.prod f₂ fun i₂ x₂ => h i₁ x₁ i₂ x₂) = Dfinsupp.prod f₂ fun i₂ x₂ => Dfinsupp.prod f₁ fun i₁ x₁ => h i₁ x₁ i₂ x₂
@[simp]
theorem Dfinsupp.sum_apply {ι : Type u} {β : ιType v} {ι₁ : Type u₁} [inst : ] {β₁ : ι₁Type v₁} [inst : (i₁ : ι₁) → Zero (β₁ i₁)] [inst : (i : ι₁) → (x : β₁ i) → Decidable (x 0)] [inst : (i : ι) → AddCommMonoid (β i)] {f : Dfinsupp fun i₁ => β₁ i₁} {g : (i₁ : ι₁) → β₁ i₁Dfinsupp fun i => β i} {i₂ : ι} :
↑() i₂ = Dfinsupp.sum f fun i₁ b => ↑(g i₁ b) i₂
theorem Dfinsupp.support_sum {ι : Type u} {β : ιType v} [dec : ] {ι₁ : Type u₁} [inst : ] {β₁ : ι₁Type v₁} [inst : (i₁ : ι₁) → Zero (β₁ i₁)] [inst : (i : ι₁) → (x : β₁ i) → Decidable (x 0)] [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] {f : Dfinsupp fun i₁ => β₁ i₁} {g : (i₁ : ι₁) → β₁ i₁Dfinsupp fun i => β i} :
Finset.bunionᵢ () fun i => Dfinsupp.support (g i (f i))
@[simp]
theorem Dfinsupp.sum_zero {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {f : Dfinsupp fun i => β i} :
(Dfinsupp.sum f fun x x => 0) = 0
@[simp]
theorem Dfinsupp.prod_one {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {f : Dfinsupp fun i => β i} :
(Dfinsupp.prod f fun x x => 1) = 1
@[simp]
theorem Dfinsupp.sum_add {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {f : Dfinsupp fun i => β i} {h₁ : (i : ι) → β iγ} {h₂ : (i : ι) → β iγ} :
(Dfinsupp.sum f fun i b => h₁ i b + h₂ i b) = Dfinsupp.sum f h₁ + Dfinsupp.sum f h₂
@[simp]
theorem Dfinsupp.prod_mul {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {f : Dfinsupp fun i => β i} {h₁ : (i : ι) → β iγ} {h₂ : (i : ι) → β iγ} :
(Dfinsupp.prod f fun i b => h₁ i b * h₂ i b) = *
@[simp]
theorem Dfinsupp.sum_neg {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {f : Dfinsupp fun i => β i} {h : (i : ι) → β iγ} :
(Dfinsupp.sum f fun i b => -h i b) = -
@[simp]
theorem Dfinsupp.prod_inv {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {f : Dfinsupp fun i => β i} {h : (i : ι) → β iγ} :
(Dfinsupp.prod f fun i b => (h i b)⁻¹) = ()⁻¹
theorem Dfinsupp.sum_eq_zero {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {f : Dfinsupp fun i => β i} {h : (i : ι) → β iγ} (hyp : ∀ (i : ι), h i (f i) = 0) :
= 0
theorem Dfinsupp.prod_eq_one {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {f : Dfinsupp fun i => β i} {h : (i : ι) → β iγ} (hyp : ∀ (i : ι), h i (f i) = 1) :
= 1
theorem Dfinsupp.smul_sum {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] {α : Type u_1} [inst : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] [inst : ] {f : Dfinsupp fun i => β i} {h : (i : ι) → β iγ} {c : α} :
c = Dfinsupp.sum f fun a b => c h a b
theorem Dfinsupp.sum_add_index {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {f : Dfinsupp fun i => β i} {g : Dfinsupp fun 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₂) :
Dfinsupp.sum (f + g) h = +
theorem Dfinsupp.prod_add_index {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {f : Dfinsupp fun i => β i} {g : Dfinsupp fun 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₂) :
Dfinsupp.prod (f + g) h = *
theorem dfinsupp_sum_mem {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {S : Type u_1} [inst : SetLike S γ] [inst : ] (s : S) (f : Dfinsupp fun i => β i) (g : (i : ι) → β iγ) (h : ∀ (c : ι), f c 0g c (f c) s) :
s
theorem dfinsupp_prod_mem {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {S : Type u_1} [inst : SetLike S γ] [inst : ] (s : S) (f : Dfinsupp fun i => β i) (g : (i : ι) → β iγ) (h : ∀ (c : ι), f c 0g c (f c) s) :
s
@[simp]
theorem Dfinsupp.sum_eq_sum_fintype {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] (v : Dfinsupp fun i => β i) {f : (i : ι) → β iγ} (hf : ∀ (i : ι), f i 0 = 0) :
= Finset.sum Finset.univ fun i => f i (Dfinsupp.equivFunOnFintype v i)
@[simp]
theorem Dfinsupp.prod_eq_prod_fintype {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] (v : Dfinsupp fun i => β i) {f : (i : ι) → β iγ} (hf : ∀ (i : ι), f i 0 = 1) :
= Finset.prod Finset.univ fun i => f i (Dfinsupp.equivFunOnFintype v i)
def Dfinsupp.sumAddHom {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] [inst : ] (φ : (i : ι) → β i →+ γ) :
(Dfinsupp fun 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.
@[simp]
theorem Dfinsupp.sumAddHom_single {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] [inst : ] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i) :
↑() () = ↑(φ i) x
@[simp]
theorem Dfinsupp.sumAddHom_comp_single {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] [inst : ] (f : (i : ι) → β i →+ γ) (i : ι) :
= f i
theorem Dfinsupp.sumAddHom_apply {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] (φ : (i : ι) → β i →+ γ) (f : Dfinsupp fun i => β i) :
↑() f = Dfinsupp.sum f 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} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] [inst : ] {S : Type u_1} [inst : SetLike S γ] [inst : ] (s : S) (f : Dfinsupp fun i => β i) (g : (i : ι) → β i →+ γ) (h : ∀ (c : ι), f c 0↑(g c) (f c) s) :
↑() f s
theorem AddSubmonoid.supᵢ_eq_mrange_dfinsupp_sumAddHom {ι : Type u} {γ : Type w} [dec : ] [inst : ] (S : ι) :

The supremum of a family of commutative additive submonoids is equal to the range of Dfinsupp.sumAddHom; that is, every element in the supᵢ 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} [dec : ] (p : ιProp) [inst : ] [inst : ] (S : ι) :

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 supᵢ 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_supᵢ_iff_exists_dfinsupp {ι : Type u} {γ : Type w} [dec : ] [inst : ] (S : ι) (x : γ) :
x supᵢ S f, ↑(Dfinsupp.sumAddHom fun i => AddSubmonoid.subtype (S i)) f = x
theorem AddSubmonoid.mem_supᵢ_iff_exists_dfinsupp' {ι : Type u} {γ : Type w} [dec : ] [inst : ] (S : ι) [inst : (i : ι) → (x : { x // x S i }) → Decidable (x 0)] (x : γ) :
x supᵢ S f, (Dfinsupp.sum f fun i xi => xi) = x

A variant of AddSubmonoid.mem_supᵢ_iff_exists_dfinsupp with the RHS fully unfolded.

theorem AddSubmonoid.mem_bsupr_iff_exists_dfinsupp {ι : Type u} {γ : Type w} [dec : ] (p : ιProp) [inst : ] [inst : ] (S : ι) (x : γ) :
(x i, _h, S i) f, ↑(Dfinsupp.sumAddHom fun i => AddSubmonoid.subtype (S i)) () = x
theorem Dfinsupp.sumAddHom_comm {ι₁ : Type u_1} {ι₂ : Type u_2} {β₁ : ι₁Type u_3} {β₂ : ι₂Type u_4} {γ : Type u_5} [inst : ] [inst : ] [inst : (i : ι₁) → AddZeroClass (β₁ i)] [inst : (i : ι₂) → AddZeroClass (β₂ i)] [inst : ] (f₁ : Dfinsupp fun i => β₁ i) (f₂ : Dfinsupp fun 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₂ => AddMonoidHom.flip (h i₁ i₂)) f₂) f₁
@[simp]
theorem Dfinsupp.liftAddHom_apply {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] [inst : ] (φ : (i : ι) → β i →+ γ) :
@[simp]
theorem Dfinsupp.liftAddHom_symm_apply {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] [inst : ] (F : (Dfinsupp fun i => β i) →+ γ) (i : ι) :
def Dfinsupp.liftAddHom {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] [inst : ] :
((i : ι) → β i →+ γ) ≃+ ((Dfinsupp fun i => β i) →+ γ)

The Dfinsupp version of Finsupp.liftAddHom,

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Dfinsupp.liftAddHom_singleAddHom {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → AddCommMonoid (β i)] :

The Dfinsupp version of Finsupp.liftAddHom_singleAddHom,

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

The Dfinsupp version of Finsupp.liftAddHom_apply_single,

theorem Dfinsupp.liftAddHom_comp_single {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] [inst : ] (f : (i : ι) → β i →+ γ) (i : ι) :

The Dfinsupp version of Finsupp.liftAddHom_comp_single,

theorem Dfinsupp.comp_liftAddHom {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] {δ : Type u_1} [inst : (i : ι) → AddZeroClass (β i)] [inst : ] [inst : ] (g : γ →+ δ) (f : (i : ι) → β i →+ γ) :

The Dfinsupp version of Finsupp.comp_liftAddHom,

@[simp]
theorem Dfinsupp.sumAddHom_zero {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] [inst : ] :
(Dfinsupp.sumAddHom fun i => 0) = 0
@[simp]
theorem Dfinsupp.sumAddHom_add {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddZeroClass (β i)] [inst : ] (g : (i : ι) → β i →+ γ) (h : (i : ι) → β i →+ γ) :
(Dfinsupp.sumAddHom fun i => g i + h i) =
@[simp]
theorem Dfinsupp.sumAddHom_singleAddHom {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → AddCommMonoid (β i)] :
= AddMonoidHom.id (Dfinsupp fun i => β i)
theorem Dfinsupp.comp_sumAddHom {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] {δ : Type u_1} [inst : (i : ι) → AddZeroClass (β i)] [inst : ] [inst : ] (g : γ →+ δ) (f : (i : ι) → β i →+ γ) :
theorem Dfinsupp.sum_sub_index {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → AddGroup (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {f : Dfinsupp fun i => β i} {g : Dfinsupp fun i => β i} {h : (i : ι) → β iγ} (h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂) :
Dfinsupp.sum (f - g) h = -
theorem Dfinsupp.sum_finset_sum_index {ι : Type u} {β : ιType v} [dec : ] {γ : Type w} {α : Type x} [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {s : } {g : αDfinsupp fun 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₂) :
(Finset.sum s fun i => Dfinsupp.sum (g i) h) = Dfinsupp.sum (Finset.sum s fun i => g i) h
theorem Dfinsupp.prod_finset_sum_index {ι : Type u} {β : ιType v} [dec : ] {γ : Type w} {α : Type x} [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {s : } {g : αDfinsupp fun 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₂) :
(Finset.prod s fun i => Dfinsupp.prod (g i) h) = Dfinsupp.prod (Finset.sum s fun i => g i) h
theorem Dfinsupp.sum_sum_index {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] {ι₁ : Type u₁} [inst : ] {β₁ : ι₁Type v₁} [inst : (i₁ : ι₁) → Zero (β₁ i₁)] [inst : (i : ι₁) → (x : β₁ i) → Decidable (x 0)] [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {f : Dfinsupp fun i₁ => β₁ i₁} {g : (i₁ : ι₁) → β₁ i₁Dfinsupp fun 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₂) :
Dfinsupp.sum () h = Dfinsupp.sum f fun i b => Dfinsupp.sum (g i b) h
theorem Dfinsupp.prod_sum_index {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] {ι₁ : Type u₁} [inst : ] {β₁ : ι₁Type v₁} [inst : (i₁ : ι₁) → Zero (β₁ i₁)] [inst : (i : ι₁) → (x : β₁ i) → Decidable (x 0)] [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {f : Dfinsupp fun i₁ => β₁ i₁} {g : (i₁ : ι₁) → β₁ i₁Dfinsupp fun 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₂) :
Dfinsupp.prod () h = Dfinsupp.prod f fun i b => Dfinsupp.prod (g i b) h
@[simp]
theorem Dfinsupp.sum_single {ι : Type u} {β : ιType v} [dec : ] [inst : (i : ι) → AddCommMonoid (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] {f : Dfinsupp fun i => β i} :
Dfinsupp.sum f Dfinsupp.single = f
abbrev Dfinsupp.sum_subtypeDomain_index.match_1 {ι : Type u_1} {p : ιProp} (motive : Prop) :
(x : ) → ((a₁ : ι) → (ha₁ : p a₁) → motive { val := a₁, property := ha₁ }) → motive x
Equations
theorem Dfinsupp.sum_subtypeDomain_index {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {v : Dfinsupp fun i => β i} {p : ιProp} [inst : ] {h : (i : ι) → β iγ} (hp : (x : ι) → p x) :
(Dfinsupp.sum () fun i b => h (i) b) =
theorem Dfinsupp.prod_subtypeDomain_index {ι : Type u} {γ : Type w} {β : ιType v} [dec : ] [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] {v : Dfinsupp fun i => β i} {p : ιProp} [inst : ] {h : (i : ι) → β iγ} (hp : (x : ι) → p x) :
(Dfinsupp.prod () fun i b => h (i) b) =
theorem Dfinsupp.subtypeDomain_sum {ι : Type u} {γ : Type w} {β : ιType v} [inst : (i : ι) → AddCommMonoid (β i)] {s : } {h : γDfinsupp fun i => β i} {p : ιProp} [inst : ] :
theorem Dfinsupp.subtypeDomain_finsupp_sum {ι : Type u} {γ : Type w} {β : ιType v} {δ : γType x} [inst : ] [inst : (c : γ) → Zero (δ c)] [inst : (c : γ) → (x : δ c) → Decidable (x 0)] [inst : (i : ι) → AddCommMonoid (β i)] {p : ιProp} [inst : ] {s : Dfinsupp fun c => δ c} {h : (c : γ) → δ cDfinsupp fun i => β i} :
= Dfinsupp.sum s fun c d => 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₂} [inst : (i : ι) → AddZeroClass (β₁ i)] [inst : (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₁ : Dfinsupp fun i => β₁ i) (g₂ : Dfinsupp fun 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₂} [inst : (i : ι) → AddZeroClass (β₁ i)] [inst : (i : ι) → AddZeroClass (β₂ i)] (f : (i : ι) → β₁ i →+ β₂ i) (x : Dfinsupp fun i => β₁ i) :
= Dfinsupp.mapRange (fun i x => ↑(f i) x) (_ : ∀ (i : ι), ↑(f i) 0 = 0) x
def Dfinsupp.mapRange.addMonoidHom {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [inst : (i : ι) → AddZeroClass (β₁ i)] [inst : (i : ι) → AddZeroClass (β₂ i)] (f : (i : ι) → β₁ i →+ β₂ i) :
(Dfinsupp fun i => β₁ i) →+ Dfinsupp fun i => β₂ i

Dfinsupp.mapRange as an AddMonoidHom.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Dfinsupp.mapRange.addMonoidHom_id {ι : Type u} {β₂ : ιType v₂} [inst : (i : ι) → AddZeroClass (β₂ i)] :
theorem Dfinsupp.mapRange.addMonoidHom_comp {ι : Type u} {β : ιType v} {β₁ : ιType v₁} {β₂ : ιType v₂} [inst : (i : ι) → AddZeroClass (β i)] [inst : (i : ι) → AddZeroClass (β₁ i)] [inst : (i : ι) → AddZeroClass (β₂ i)] (f : (i : ι) → β₁ i →+ β₂ i) (f₂ : (i : ι) → β i →+ β₁ i) :
@[simp]
theorem Dfinsupp.mapRange.addEquiv_apply {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [inst : (i : ι) → AddZeroClass (β₁ i)] [inst : (i : ι) → AddZeroClass (β₂ i)] (e : (i : ι) → β₁ i ≃+ β₂ i) (x : Dfinsupp fun i => β₁ i) :
= Dfinsupp.mapRange (fun i x => ↑(e i) x) (_ : ∀ (i : ι), ↑(e i) 0 = 0) x
def Dfinsupp.mapRange.addEquiv {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [inst : (i : ι) → AddZeroClass (β₁ i)] [inst : (i : ι) → AddZeroClass (β₂ i)] (e : (i : ι) → β₁ i ≃+ β₂ i) :
(Dfinsupp fun i => β₁ i) ≃+ Dfinsupp fun i => β₂ i

Dfinsupp.mapRange.addMonoidHom as an AddEquiv.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Dfinsupp.mapRange.addEquiv_refl {ι : Type u} {β₁ : ιType v₁} [inst : (i : ι) → AddZeroClass (β₁ i)] :
theorem Dfinsupp.mapRange.addEquiv_trans {ι : Type u} {β : ιType v} {β₁ : ιType v₁} {β₂ : ιType v₂} [inst : (i : ι) → AddZeroClass (β i)] [inst : (i : ι) → AddZeroClass (β₁ i)] [inst : (i : ι) → AddZeroClass (β₂ i)] (f : (i : ι) → β i ≃+ β₁ i) (f₂ : (i : ι) → β₁ i ≃+ β₂ i) :
@[simp]
theorem Dfinsupp.mapRange.addEquiv_symm {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [inst : (i : ι) → AddZeroClass (β₁ i)] [inst : (i : ι) → AddZeroClass (β₂ i)] (e : (i : ι) → β₁ i ≃+ β₂ i) :

### 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.map_dfinsupp_sum {ι : Type u} {β : ιType v} [inst : ] {R : Type u_1} {S : Type u_2} [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] [inst : ] (h : R →+ S) (f : Dfinsupp fun i => β i) (g : (i : ι) → β iR) :
h () = Dfinsupp.sum f fun a b => h (g a b)
@[simp]
theorem MonoidHom.map_dfinsupp_prod {ι : Type u} {β : ιType v} [inst : ] {R : Type u_1} {S : Type u_2} [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] [inst : ] (h : R →* S) (f : Dfinsupp fun i => β i) (g : (i : ι) → β iR) :
h () = Dfinsupp.prod f fun a b => h (g a b)
theorem AddMonoidHom.coe_dfinsupp_sum {ι : Type u} {β : ιType v} [inst : ] {R : Type u_1} {S : Type u_2} [inst : (i : ι) → Zero (β i)] [inst : (i : ι) → (x : β i) → Decidable (x 0)] [inst : ] [inst : ] (f : Dfinsupp fun i => β i) (g : (i : ι) → β iR →+ S) :
↑() = Dfinsupp.sum f fun a b => ↑(g a b)
theorem MonoidHom.coe_dfinsupp_prod {ι : Type u} {β : ιType v} [inst : ] {R : Type u_1} {S : Type u_2} [inst : (i : ι) →