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 (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 : Multiset ι // ∀ (i : ι), i ∈ s ∨ self.toFun i = 0 }
The support of a dependent function with finite support (aka DFinsupp).

)

Instances For

def «termΠ₀_,_».delab :

Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

One or more equations did not get rendered due to their size.

def «termΠ₀_,_» :

Lean.ParserDescr

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

def «term_→ₚ_» :

Lean.TrailingParserDescr

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.

Equations

«term_→ₚ_» = Lean.ParserDescr.trailingNode `term_→ₚ_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ₚ ") (Lean.ParserDescr.cat `term 26))

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.instCoeFunDFinsuppForAll {ι : 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.instCoeFunDFinsuppForAll = inferInstance

@[simp]

theorem DFinsupp.toFun_eq_coe {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] (f : Π₀ (i : ι), β i) :

f.toFun = ⇑f

theorem DFinsupp.ext {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] {f : Π₀ (i : ι), β i} {g : Π₀ (i : ι), β i} (h : ∀ (i : ι), f i = g i) :

f = g

@[deprecated DFunLike.ext_iff]

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.ne_iff {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] {f : Π₀ (i : ι), β i} {g : Π₀ (i : ι), β i} :

f ≠ g ↔ ∃ (i : ι), f i ≠ g i

@[deprecated DFunLike.coe_injective]

theorem DFinsupp.coeFn_injective {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] :

Function.Injective DFunLike.coe

instance DFinsupp.instZeroDFinsupp {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] :

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

Equations

DFinsupp.instZeroDFinsupp = { zero := { toFun := 0, support' := Trunc.mk { val := ∅, property := ⋯ } } }

instance DFinsupp.instInhabitedDFinsupp {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] :

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

Equations

DFinsupp.instInhabitedDFinsupp = { default := 0 }

@[simp]

theorem DFinsupp.coe_mk' {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] (f : (i : ι) → β i) (s : Trunc { s : Multiset ι // ∀ (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

One or more equations did not get rendered due to their size.

@[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) :

DFinsupp.mapRange f hf 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.

@[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

DFinsupp.piecewise x y s = DFinsupp.zipWith (fun (i : ι) (x y : β i) => if i ∈ s then x else y) ⋯ x y

theorem DFinsupp.piecewise_apply {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] (x : Π₀ (i : ι), β i) (y : Π₀ (i : ι), β i) (s : Set ι) [(i : ι) → Decidable (i ∈ s)] (i : ι) :

(DFinsupp.piecewise x 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)] :

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

instance DFinsupp.instAddDFinsuppToZero {ι : Type u} {β : ι → Type v} [(i : ι) → AddZeroClass (β i)] :

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

Equations

DFinsupp.instAddDFinsuppToZero = { 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

DFinsupp.addZeroClass = Function.Injective.addZeroClass (fun (f : Π₀ (i : ι), β i) => ⇑f) ⋯ ⋯ ⋯

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.instAddMonoidDFinsuppToZero {ι : Type u} {β : ι → Type v} [(i : ι) → AddMonoid (β i)] :

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

Equations

DFinsupp.instAddMonoidDFinsuppToZero = Function.Injective.addMonoid (fun (f : Π₀ (i : ι), β i) => ⇑f) ⋯ ⋯ ⋯ ⋯

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 = { toZeroHom := { toFun := DFunLike.coe, map_zero' := ⋯ }, map_add' := ⋯ }

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

DFinsupp.evalAddMonoidHom i = AddMonoidHom.comp (Pi.evalAddMonoidHom β i) DFinsupp.coeFnAddMonoidHom

instance DFinsupp.addCommMonoid {ι : Type u} {β : ι → Type v} [(i : ι) → AddCommMonoid (β i)] :

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

Equations

DFinsupp.addCommMonoid = Function.Injective.addCommMonoid (fun (f : Π₀ (i : ι), β i) => ⇑f) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem DFinsupp.coe_finset_sum {ι : Type u} {β : ι → Type v} {α : Type u_1} [(i : ι) → AddCommMonoid (β i)] (s : Finset α) (g : α → Π₀ (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} [(i : ι) → AddCommMonoid (β i)] (s : Finset α) (g : α → Π₀ (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} [(i : ι) → AddGroup (β i)] :

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

Equations

DFinsupp.instNegDFinsuppToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoid = { 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.instSubDFinsuppToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoid {ι : Type u} {β : ι → Type v} [(i : ι) → AddGroup (β i)] :

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

Equations

DFinsupp.instSubDFinsuppToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoid = { sub := DFinsupp.zipWith (fun (x : ι) => Sub.sub) ⋯ }

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.instAddGroupDFinsuppToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoid {ι : Type u} {β : ι → Type v} [(i : ι) → AddGroup (β i)] :

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

Equations

DFinsupp.instAddGroupDFinsuppToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoid = Function.Injective.addGroup (fun (f : Π₀ (i : ι), β i) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance DFinsupp.addCommGroup {ι : Type u} {β : ι → Type v} [(i : ι) → AddCommGroup (β i)] :

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

Equations

DFinsupp.addCommGroup = Function.Injective.addCommGroup (fun (f : Π₀ (i : ι), β i) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance DFinsupp.instSMulDFinsuppToZero {ι : Type u} {γ : Type w} {β : ι → Type v} [Monoid γ] [(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.instSMulDFinsuppToZero = { 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} [Monoid γ] [(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} [Monoid γ] [(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} [Monoid γ] [Monoid δ] [(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} [Monoid γ] [Monoid δ] [(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} [Monoid γ] [(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} [Monoid γ] [(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

DFinsupp.distribMulAction = Function.Injective.distribMulAction DFinsupp.coeFnAddMonoidHom ⋯ ⋯

instance DFinsupp.module {ι : Type u} {γ : Type w} {β : ι → Type v} [Semiring γ] [(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

DFinsupp.module = let __src := inferInstanceAs (DistribMulAction γ (Π₀ (i : ι), β i)); Module.mk ⋯ ⋯

def DFinsupp.filter {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] (p : ι → Prop) [DecidablePred p] (x : Π₀ (i : ι), β i) :

Π₀ (i : ι), β i

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

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem DFinsupp.filter_apply {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] (p : ι → Prop) [DecidablePred p] (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} [DecidablePred p] (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} [DecidablePred p] (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) [DecidablePred p] :

DFinsupp.filter p f + DFinsupp.filter (fun (i : ι) => ¬p i) f = f

@[simp]

theorem DFinsupp.filter_zero {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] (p : ι → Prop) [DecidablePred p] :

DFinsupp.filter p 0 = 0

@[simp]

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

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

@[simp]

theorem DFinsupp.filter_smul {ι : Type u} {γ : Type w} {β : ι → Type v} [Monoid γ] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] (p : ι → Prop) [DecidablePred p] (r : γ) (f : Π₀ (i : ι), β i) :

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

@[simp]

theorem DFinsupp.filterAddMonoidHom_apply {ι : Type u} (β : ι → Type v) [(i : ι) → AddZeroClass (β i)] (p : ι → Prop) [DecidablePred p] (x : Π₀ (i : ι), β i) :

(DFinsupp.filterAddMonoidHom β p) x = DFinsupp.filter p x

def DFinsupp.filterAddMonoidHom {ι : Type u} (β : ι → Type v) [(i : ι) → AddZeroClass (β i)] (p : ι → Prop) [DecidablePred p] :

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

DFinsupp.filter as an AddMonoidHom.

Equations

DFinsupp.filterAddMonoidHom β p = { toZeroHom := { toFun := DFinsupp.filter p, map_zero' := ⋯ }, map_add' := ⋯ }

@[simp]

theorem DFinsupp.filterLinearMap_apply {ι : Type u} (γ : Type w) (β : ι → Type v) [Semiring γ] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module γ (β i)] (p : ι → Prop) [DecidablePred p] (x : Π₀ (i : ι), β i) :

(DFinsupp.filterLinearMap γ β p) x = DFinsupp.filter p x

def DFinsupp.filterLinearMap {ι : Type u} (γ : Type w) (β : ι → Type v) [Semiring γ] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module γ (β i)] (p : ι → Prop) [DecidablePred p] :

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

DFinsupp.filter as a LinearMap.

Equations

DFinsupp.filterLinearMap γ β p = { toAddHom := { toFun := DFinsupp.filter p, map_add' := ⋯ }, map_smul' := ⋯ }

@[simp]

theorem DFinsupp.filter_neg {ι : Type u} {β : ι → Type v} [(i : ι) → AddGroup (β i)] (p : ι → Prop) [DecidablePred p] (f : Π₀ (i : ι), β i) :

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

@[simp]

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

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

def DFinsupp.subtypeDomain {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] (p : ι → Prop) [DecidablePred p] (x : Π₀ (i : ι), β i) :

Π₀ (i : Subtype p), β ↑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} [(i : ι) → Zero (β i)] {p : ι → Prop} [DecidablePred p] :

DFinsupp.subtypeDomain p 0 = 0

@[simp]

theorem DFinsupp.subtypeDomain_apply {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] {p : ι → Prop} [DecidablePred p] {i : Subtype p} {v : Π₀ (i : ι), β i} :

(DFinsupp.subtypeDomain p v) i = v ↑i

@[simp]

theorem DFinsupp.subtypeDomain_add {ι : Type u} {β : ι → Type v} [(i : ι) → AddZeroClass (β i)] {p : ι → Prop} [DecidablePred p] (v : Π₀ (i : ι), β i) (v' : Π₀ (i : ι), β i) :

DFinsupp.subtypeDomain p (v + v') = DFinsupp.subtypeDomain p v + DFinsupp.subtypeDomain p v'

@[simp]

theorem DFinsupp.subtypeDomain_smul {ι : Type u} {γ : Type w} {β : ι → Type v} [Monoid γ] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] {p : ι → Prop} [DecidablePred p] (r : γ) (f : Π₀ (i : ι), β i) :

DFinsupp.subtypeDomain p (r • f) = r • DFinsupp.subtypeDomain p f

@[simp]

theorem DFinsupp.subtypeDomainAddMonoidHom_apply {ι : Type u} (β : ι → Type v) [(i : ι) → AddZeroClass (β i)] (p : ι → Prop) [DecidablePred p] (x : Π₀ (i : ι), β i) :

(DFinsupp.subtypeDomainAddMonoidHom β p) x = DFinsupp.subtypeDomain p x

def DFinsupp.subtypeDomainAddMonoidHom {ι : Type u} (β : ι → Type v) [(i : ι) → AddZeroClass (β i)] (p : ι → Prop) [DecidablePred p] :

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

subtypeDomain but as an AddMonoidHom.

Equations

DFinsupp.subtypeDomainAddMonoidHom β p = { toZeroHom := { toFun := DFinsupp.subtypeDomain p, map_zero' := ⋯ }, map_add' := ⋯ }

@[simp]

theorem DFinsupp.subtypeDomainLinearMap_apply {ι : Type u} (γ : Type w) (β : ι → Type v) [Semiring γ] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module γ (β i)] (p : ι → Prop) [DecidablePred p] (x : Π₀ (i : ι), β i) :

(DFinsupp.subtypeDomainLinearMap γ β p) x = DFinsupp.subtypeDomain p x

def DFinsupp.subtypeDomainLinearMap {ι : Type u} (γ : Type w) (β : ι → Type v) [Semiring γ] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module γ (β i)] (p : ι → Prop) [DecidablePred p] :

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

DFinsupp.subtypeDomain as a LinearMap.

Equations

DFinsupp.subtypeDomainLinearMap γ β p = { toAddHom := { toFun := DFinsupp.subtypeDomain p, map_add' := ⋯ }, map_smul' := ⋯ }

@[simp]

theorem DFinsupp.subtypeDomain_neg {ι : Type u} {β : ι → Type v} [(i : ι) → AddGroup (β i)] {p : ι → Prop} [DecidablePred p] {v : Π₀ (i : ι), β i} :

DFinsupp.subtypeDomain p (-v) = -DFinsupp.subtypeDomain p v

@[simp]

theorem DFinsupp.subtypeDomain_sub {ι : Type u} {β : ι → Type v} [(i : ι) → AddGroup (β i)] {p : ι → Prop} [DecidablePred p] {v : Π₀ (i : ι), β i} {v' : Π₀ (i : ι), β i} :

DFinsupp.subtypeDomain p (v - v') = DFinsupp.subtypeDomain p v - DFinsupp.subtypeDomain p v'

theorem DFinsupp.finite_support {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] (f : Π₀ (i : ι), β i) :

Set.Finite {i : ι | f i ≠ 0}

def DFinsupp.mk {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] (s : Finset ι) (x : (i : ↑↑s) → β ↑i) :

Π₀ (i : ι), β i

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

Equations

DFinsupp.mk s x = { toFun := fun (i : ι) => if H : i ∈ s then x { val := i, property := H } else 0, support' := Trunc.mk { val := s.val, property := ⋯ } }

@[simp]

theorem DFinsupp.mk_apply {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] {s : Finset ι} {x : (i : ↑↑s) → β ↑i} {i : ι} :

(DFinsupp.mk s x) i = if H : i ∈ s then x { val := i, property := H } else 0

theorem DFinsupp.mk_of_mem {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] {s : Finset ι} {x : (i : ↑↑s) → β ↑i} {i : ι} (hi : i ∈ s) :

(DFinsupp.mk s x) i = x { val := i, property := hi }

theorem DFinsupp.mk_of_not_mem {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] {s : Finset ι} {x : (i : ↑↑s) → β ↑i} {i : ι} (hi : i ∉ s) :

(DFinsupp.mk s x) i = 0

theorem DFinsupp.mk_injective {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] (s : Finset ι) :

Function.Injective (DFinsupp.mk s)

instance DFinsupp.unique {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [∀ (i : ι), Subsingleton (β i)] :

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

Equations

DFinsupp.unique = Function.Injective.unique ⋯

instance DFinsupp.uniqueOfIsEmpty {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [IsEmpty ι] :

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

Equations

DFinsupp.uniqueOfIsEmpty = Function.Injective.unique ⋯

@[simp]

theorem DFinsupp.equivFunOnFintype_apply {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [Fintype ι] :

∀ (a : Π₀ (i : ι), (fun (i : ι) => β i) i) (a_1 : ι), DFinsupp.equivFunOnFintype a a_1 = a a_1

def DFinsupp.equivFunOnFintype {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [Fintype ι] :

(Π₀ (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} [(i : ι) → Zero (β i)] [Fintype ι] (f : Π₀ (i : ι), β i) :

DFinsupp.equivFunOnFintype.symm ⇑f = f

def DFinsupp.single {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(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

DFinsupp.single i b = { toFun := Pi.single i b, support' := Trunc.mk { val := {i}, property := ⋯ } }

theorem DFinsupp.single_eq_pi_single {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] {i : ι} {b : β i} :

⇑(DFinsupp.single i b) = Pi.single i b

@[simp]

theorem DFinsupp.single_apply {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(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} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] (i : ι) :

DFinsupp.single i 0 = 0

theorem DFinsupp.single_eq_same {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] {i : ι} {b : β i} :

(DFinsupp.single i b) i = b

theorem DFinsupp.single_eq_of_ne {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] {i : ι} {i' : ι} {b : β i} (h : i ≠ i') :

(DFinsupp.single i b) i' = 0

theorem DFinsupp.single_injective {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] {i : ι} :

Function.Injective (DFinsupp.single i)

theorem DFinsupp.single_eq_single_iff {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] (i : ι) (j : ι) (xi : β i) (xj : β j) :

DFinsupp.single i xi = DFinsupp.single j xj ↔ 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 : DecidableEq ι] [(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} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] {i : ι} {xi : β i} :

DFinsupp.single i xi = 0 ↔ xi = 0

theorem DFinsupp.filter_single {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] (p : ι → Prop) [DecidablePred p] (i : ι) (x : β i) :

DFinsupp.filter p (DFinsupp.single i x) = if p i then DFinsupp.single i x else 0

@[simp]

theorem DFinsupp.filter_single_pos {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] {p : ι → Prop} [DecidablePred p] (i : ι) (x : β i) (h : p i) :

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

@[simp]

theorem DFinsupp.filter_single_neg {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] {p : ι → Prop} [DecidablePred p] (i : ι) (x : β i) (h : ¬p i) :

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

theorem DFinsupp.single_eq_of_sigma_eq {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] {i : ι} {j : ι} {xi : β i} {xj : β j} (h : { fst := i, snd := xi } = { fst := j, snd := xj }) :

DFinsupp.single i xi = DFinsupp.single 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} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [Fintype ι] (i : ι) (m : β i) :

DFinsupp.equivFunOnFintype (DFinsupp.single i m) = Pi.single i m

@[simp]

theorem DFinsupp.equivFunOnFintype_symm_single {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [Fintype ι] (i : ι) (m : β i) :

DFinsupp.equivFunOnFintype.symm (Pi.single i m) = DFinsupp.single i m

@[simp]

theorem DFinsupp.zipWith_single_single {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [dec : DecidableEq ι] [(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} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] (i : ι) (x : Π₀ (i : ι), β i) :

Π₀ (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 : DecidableEq ι] [(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} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] {i : ι} {f : Π₀ (i : ι), β i} :

(DFinsupp.erase i f) i = 0

theorem DFinsupp.erase_ne {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(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} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] (x : Π₀ (i : ι), β i) (i : ι) [(i' : ι) → Decidable (i' ∈ {i})] :

DFinsupp.piecewise (DFinsupp.single i (x i)) (DFinsupp.erase i x) {i} = x

theorem DFinsupp.erase_eq_sub_single {ι : Type u} [dec : DecidableEq ι] {β : ι → Type u_1} [(i : ι) → AddGroup (β i)] (f : Π₀ (i : ι), β i) (i : ι) :

DFinsupp.erase i f = f - DFinsupp.single i (f i)

@[simp]

theorem DFinsupp.erase_zero {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] (i : ι) :

DFinsupp.erase i 0 = 0

@[simp]

theorem DFinsupp.filter_ne_eq_erase {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] (f : Π₀ (i : ι), β i) (i : ι) :

DFinsupp.filter (fun (x : ι) => x ≠ i) f = DFinsupp.erase i f

@[simp]

theorem DFinsupp.filter_ne_eq_erase' {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] (f : Π₀ (i : ι), β i) (i : ι) :

DFinsupp.filter (fun (x : ι) => i ≠ x) f = DFinsupp.erase i f

theorem DFinsupp.erase_single {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] (j : ι) (i : ι) (x : β i) :

DFinsupp.erase j (DFinsupp.single i x) = if i = j then 0 else DFinsupp.single i x

@[simp]

theorem DFinsupp.erase_single_same {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] (i : ι) (x : β i) :

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

@[simp]

theorem DFinsupp.erase_single_ne {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] {i : ι} {j : ι} (x : β i) (h : i ≠ j) :

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

def DFinsupp.update {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] (i : ι) (f : Π₀ (i : ι), β i) (b : β i) :

Π₀ (i : ι), β i

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

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

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem DFinsupp.coe_update {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] (i : ι) (f : Π₀ (i : ι), β i) (b : β i) :

⇑(DFinsupp.update i f b) = Function.update (⇑f) i b

@[simp]

theorem DFinsupp.update_self {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] (i : ι) (f : Π₀ (i : ι), β i) :

DFinsupp.update i f (f i) = f

@[simp]

theorem DFinsupp.update_eq_erase {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] (i : ι) (f : Π₀ (i : ι), β i) :

DFinsupp.update i f 0 = DFinsupp.erase i f

theorem DFinsupp.update_eq_single_add_erase {ι : Type u} [dec : DecidableEq ι] {β : ι → Type u_1} [(i : ι) → AddZeroClass (β i)] (f : Π₀ (i : ι), β i) (i : ι) (b : β i) :

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

theorem DFinsupp.update_eq_erase_add_single {ι : Type u} [dec : DecidableEq ι] {β : ι → Type u_1} [(i : ι) → AddZeroClass (β i)] (f : Π₀ (i : ι), β i) (i : ι) (b : β i) :

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

theorem DFinsupp.update_eq_sub_add_single {ι : Type u} [dec : DecidableEq ι] {β : ι → Type u_1} [(i : ι) → AddGroup (β i)] (f : Π₀ (i : ι), β i) (i : ι) (b : β i) :

DFinsupp.update i f b = f - DFinsupp.single i (f i) + DFinsupp.single i b

@[simp]

theorem DFinsupp.single_add {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] (i : ι) (b₁ : β i) (b₂ : β i) :

DFinsupp.single i (b₁ + b₂) = DFinsupp.single i b₁ + DFinsupp.single i b₂

@[simp]

theorem DFinsupp.erase_add {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] (i : ι) (f₁ : Π₀ (i : ι), β i) (f₂ : Π₀ (i : ι), β i) :

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

@[simp]

theorem DFinsupp.singleAddHom_apply {ι : Type u} (β : ι → Type v) [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] (i : ι) (b : β i) :

(DFinsupp.singleAddHom β i) b = DFinsupp.single i b

def DFinsupp.singleAddHom {ι : Type u} (β : ι → Type v) [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] (i : ι) :

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

DFinsupp.single as an AddMonoidHom.

Equations

DFinsupp.singleAddHom β i = { toZeroHom := { toFun := DFinsupp.single i, map_zero' := ⋯ }, map_add' := ⋯ }

@[simp]

theorem DFinsupp.eraseAddHom_apply {ι : Type u} (β : ι → Type v) [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] (i : ι) (x : Π₀ (i : ι), β i) :

(DFinsupp.eraseAddHom β i) x = DFinsupp.erase i x

def DFinsupp.eraseAddHom {ι : Type u} (β : ι → Type v) [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] (i : ι) :

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

DFinsupp.erase as an AddMonoidHom.

Equations

DFinsupp.eraseAddHom β i = { toZeroHom := { toFun := DFinsupp.erase i, map_zero' := ⋯ }, map_add' := ⋯ }

@[simp]

theorem DFinsupp.single_neg {ι : Type u} [dec : DecidableEq ι] {β : ι → Type v} [(i : ι) → AddGroup (β i)] (i : ι) (x : β i) :

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

@[simp]

theorem DFinsupp.single_sub {ι : Type u} [dec : DecidableEq ι] {β : ι → Type v} [(i : ι) → AddGroup (β i)] (i : ι) (x : β i) (y : β i) :

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

@[simp]

theorem DFinsupp.erase_neg {ι : Type u} [dec : DecidableEq ι] {β : ι → Type v} [(i : ι) → AddGroup (β i)] (i : ι) (f : Π₀ (i : ι), β i) :

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

@[simp]

theorem DFinsupp.erase_sub {ι : Type u} [dec : DecidableEq ι] {β : ι → Type v} [(i : ι) → AddGroup (β i)] (i : ι) (f : Π₀ (i : ι), β i) (g : Π₀ (i : ι), β i) :

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

theorem DFinsupp.single_add_erase {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] (i : ι) (f : Π₀ (i : ι), β i) :

DFinsupp.single i (f i) + DFinsupp.erase i f = f

theorem DFinsupp.erase_add_single {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] (i : ι) (f : Π₀ (i : ι), β i) :

DFinsupp.erase i f + DFinsupp.single i (f i) = f

theorem DFinsupp.induction {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] {p : (Π₀ (i : ι), β i) → Prop} (f : Π₀ (i : ι), β i) (h0 : p 0) (ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (DFinsupp.single i b + f)) :

p f

theorem DFinsupp.induction₂ {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] {p : (Π₀ (i : ι), β i) → Prop} (f : Π₀ (i : ι), β i) (h0 : p 0) (ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (f + DFinsupp.single i b)) :

p f

@[simp]

theorem DFinsupp.add_closure_iUnion_range_single {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] :

AddSubmonoid.closure (⋃ (i : ι), Set.range (DFinsupp.single i)) = ⊤

theorem DFinsupp.addHom_ext {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] {γ : Type w} [AddZeroClass γ] ⦃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' {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] {γ : Type w} [AddZeroClass γ] ⦃f : (Π₀ (i : ι), β i) →+ γ⦄ ⦃g : (Π₀ (i : ι), β i) →+ γ⦄ (H : ∀ (x : ι), AddMonoidHom.comp f (DFinsupp.singleAddHom β x) = AddMonoidHom.comp g (DFinsupp.singleAddHom β 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 : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] {s : Finset ι} {x : (i : ↑↑s) → β ↑i} {y : (i : ↑↑s) → β ↑i} :

DFinsupp.mk s (x + y) = DFinsupp.mk s x + DFinsupp.mk s y

@[simp]

theorem DFinsupp.mk_zero {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] {s : Finset ι} :

DFinsupp.mk s 0 = 0

@[simp]

theorem DFinsupp.mk_neg {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddGroup (β i)] {s : Finset ι} {x : (i : ↑↑s) → β ↑i} :

DFinsupp.mk s (-x) = -DFinsupp.mk s x

@[simp]

theorem DFinsupp.mk_sub {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddGroup (β i)] {s : Finset ι} {x : (i : ↑↑s) → β ↑i} {y : (i : ↑↑s) → β ↑i} :

DFinsupp.mk s (x - y) = DFinsupp.mk s x - DFinsupp.mk s y

def DFinsupp.mkAddGroupHom {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddGroup (β i)] (s : Finset ι) :

((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} β_{i}$ to $\prod_{i : ι} β_{i} .$

Equations

DFinsupp.mkAddGroupHom s = { toZeroHom := { toFun := DFinsupp.mk s, map_zero' := ⋯ }, map_add' := ⋯ }

@[simp]

theorem DFinsupp.mk_smul {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [Monoid γ] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] {s : Finset ι} (c : γ) (x : (i : ↑↑s) → β ↑i) :

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

@[simp]

theorem DFinsupp.single_smul {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [Monoid γ] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] {i : ι} (c : γ) (x : β i) :

DFinsupp.single i (c • x) = c • DFinsupp.single i x

def DFinsupp.support {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(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.

@[simp]

theorem DFinsupp.support_mk_subset {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {s : Finset ι} {x : (i : ↑↑s) → β ↑i} :

DFinsupp.support (DFinsupp.mk s x) ⊆ s

@[simp]

theorem DFinsupp.support_mk'_subset {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : (i : ι) → β i} {s : Multiset ι} {h : ∀ (i : ι), i ∈ s ∨ f i = 0} :

DFinsupp.support { toFun := f, support' := Trunc.mk { val := s, property := h } } ⊆ Multiset.toFinset s

@[simp]

theorem DFinsupp.mem_support_toFun {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (f : Π₀ (i : ι), β i) (i : ι) :

i ∈ DFinsupp.support f ↔ f i ≠ 0

theorem DFinsupp.eq_mk_support {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (f : Π₀ (i : ι), β i) :

f = DFinsupp.mk (DFinsupp.support f) fun (i : ↑↑(DFinsupp.support f)) => f ↑i

@[simp]

theorem DFinsupp.subtypeSupportEqEquiv_symm_apply_coe {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (s : Finset ι) (f : (i : { x : ι // x ∈ s }) → { x : β ↑i // x ≠ 0 }) :

↑((DFinsupp.subtypeSupportEqEquiv s).symm f) = DFinsupp.mk s fun (i : ↑↑s) => ↑(f i)

@[simp]

theorem DFinsupp.subtypeSupportEqEquiv_apply_coe {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (s : Finset ι) :

∀ (x : { f : Π₀ (i : ι), β i // DFinsupp.support f = s }) (i : { x : ι // x ∈ s }), ↑((DFinsupp.subtypeSupportEqEquiv s) x i) = ↑x ↑i

def DFinsupp.subtypeSupportEqEquiv {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (s : Finset ι) :

{ f : Π₀ (i : ι), β i // DFinsupp.support f = 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.

@[simp]

theorem DFinsupp.sigmaFinsetFunEquiv_apply_snd_coe {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(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

@[simp]

theorem DFinsupp.sigmaFinsetFunEquiv_apply_fst {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] :

∀ (a : Π₀ (i : ι), β i), (DFinsupp.sigmaFinsetFunEquiv a).fst = DFinsupp.support a

def DFinsupp.sigmaFinsetFunEquiv {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] :

(Π₀ (i : ι), β i) ≃ (s : Finset ι) × ((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

DFinsupp.sigmaFinsetFunEquiv = (Equiv.sigmaFiberEquiv DFinsupp.support).symm.trans (Equiv.sigmaCongrRight DFinsupp.subtypeSupportEqEquiv)

@[simp]

theorem DFinsupp.support_zero {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] :

DFinsupp.support 0 = ∅

theorem DFinsupp.mem_support_iff {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), β i} {i : ι} :

i ∈ DFinsupp.support f ↔ f i ≠ 0

theorem DFinsupp.not_mem_support_iff {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), β i} {i : ι} :

i ∉ DFinsupp.support f ↔ f i = 0

@[simp]

theorem DFinsupp.support_eq_empty {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), β i} :

DFinsupp.support f = ∅ ↔ f = 0

instance DFinsupp.decidableZero {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] :

DecidablePred (Eq 0)

Equations

DFinsupp.decidableZero x = decidable_of_iff (DFinsupp.support x = ∅) ⋯

theorem DFinsupp.support_subset_iff {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {s : Set ι} {f : Π₀ (i : ι), β i} :

↑(DFinsupp.support f) ⊆ s ↔ ∀ i ∉ s, f i = 0

theorem DFinsupp.support_single_ne_zero {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {i : ι} {b : β i} (hb : b ≠ 0) :

DFinsupp.support (DFinsupp.single i b) = {i}

theorem DFinsupp.support_single_subset {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {i : ι} {b : β i} :

DFinsupp.support (DFinsupp.single i b) ⊆ {i}

theorem DFinsupp.mapRange_def {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [dec : DecidableEq ι] [(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.mapRange f hf g = DFinsupp.mk (DFinsupp.support g) fun (i : ↑↑(DFinsupp.support g)) => f (↑i) (g ↑i)

@[simp]

theorem DFinsupp.mapRange_single {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [dec : DecidableEq ι] [(i : ι) → Zero (β₁ i)] [(i : ι) → Zero (β₂ i)] {f : (i : ι) → β₁ i → β₂ i} {hf : ∀ (i : ι), f i 0 = 0} {i : ι} {b : β₁ i} :

DFinsupp.mapRange f hf (DFinsupp.single i b) = DFinsupp.single i (f i b)

theorem DFinsupp.support_mapRange {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [dec : DecidableEq ι] [(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.support (DFinsupp.mapRange f hf g) ⊆ DFinsupp.support g

theorem DFinsupp.zipWith_def {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [dec : DecidableEq ι] [(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 (DFinsupp.support g₁ ∪ DFinsupp.support g₂) fun (i : ↑↑(DFinsupp.support g₁ ∪ DFinsupp.support g₂)) => f (↑i) (g₁ ↑i) (g₂ ↑i)

theorem DFinsupp.support_zipWith {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [dec : DecidableEq ι] [(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.support (DFinsupp.zipWith f hf g₁ g₂) ⊆ DFinsupp.support g₁ ∪ DFinsupp.support g₂

theorem DFinsupp.erase_def {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (i : ι) (f : Π₀ (i : ι), β i) :

DFinsupp.erase i f = DFinsupp.mk (Finset.erase (DFinsupp.support f) i) fun (j : ↑↑(Finset.erase (DFinsupp.support f) i)) => f ↑j

@[simp]

theorem DFinsupp.support_erase {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (i : ι) (f : Π₀ (i : ι), β i) :

DFinsupp.support (DFinsupp.erase i f) = Finset.erase (DFinsupp.support f) i

theorem DFinsupp.support_update_ne_zero {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (f : Π₀ (i : ι), β i) (i : ι) {b : β i} (h : b ≠ 0) :

DFinsupp.support (DFinsupp.update i f b) = insert i (DFinsupp.support f)

theorem DFinsupp.support_update {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (f : Π₀ (i : ι), β i) (i : ι) (b : β i) [Decidable (b = 0)] :

DFinsupp.support (DFinsupp.update i f b) = if b = 0 then DFinsupp.support (DFinsupp.erase i f) else insert i (DFinsupp.support f)

theorem DFinsupp.filter_def {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {p : ι → Prop} [DecidablePred p] (f : Π₀ (i : ι), β i) :

DFinsupp.filter p f = DFinsupp.mk (Finset.filter p (DFinsupp.support f)) fun (i : ↑↑(Finset.filter p (DFinsupp.support f))) => f ↑i

@[simp]

theorem DFinsupp.support_filter {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {p : ι → Prop} [DecidablePred p] (f : Π₀ (i : ι), β i) :

DFinsupp.support (DFinsupp.filter p f) = Finset.filter p (DFinsupp.support f)

theorem DFinsupp.subtypeDomain_def {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {p : ι → Prop} [DecidablePred p] (f : Π₀ (i : ι), β i) :

DFinsupp.subtypeDomain p f = DFinsupp.mk (Finset.subtype p (DFinsupp.support f)) fun (i : ↑↑(Finset.subtype p (DFinsupp.support f))) => f ↑↑i

@[simp]

theorem DFinsupp.support_subtypeDomain {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {p : ι → Prop} [DecidablePred p] {f : Π₀ (i : ι), β i} :

DFinsupp.support (DFinsupp.subtypeDomain p f) = Finset.subtype p (DFinsupp.support f)

theorem DFinsupp.support_add {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {g₁ : Π₀ (i : ι), β i} {g₂ : Π₀ (i : ι), β i} :

DFinsupp.support (g₁ + g₂) ⊆ DFinsupp.support g₁ ∪ DFinsupp.support g₂

@[simp]

theorem DFinsupp.support_neg {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddGroup (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), β i} :

DFinsupp.support (-f) = DFinsupp.support f

theorem DFinsupp.support_smul {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] {γ : Type w} [Semiring γ] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module γ (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (b : γ) (v : Π₀ (i : ι), β i) :

DFinsupp.support (b • v) ⊆ DFinsupp.support v

instance DFinsupp.instDecidableEqDFinsupp {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] :

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

Equations

DFinsupp.instDecidableEqDFinsupp f g = decidable_of_iff (DFinsupp.support f = DFinsupp.support g ∧ ∀ i ∈ DFinsupp.support f, f i = g i) ⋯

noncomputable def DFinsupp.comapDomain {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] {κ : Type u_1} [(i : ι) → Zero (β i)] (h : κ → ι) (hh : Function.Injective h) (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.

@[simp]

theorem DFinsupp.comapDomain_apply {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] {κ : Type u_1} [(i : ι) → Zero (β i)] (h : κ → ι) (hh : Function.Injective h) (f : Π₀ (i : ι), β i) (k : κ) :

(DFinsupp.comapDomain h hh f) k = f (h k)

@[simp]

theorem DFinsupp.comapDomain_zero {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] {κ : Type u_1} [(i : ι) → Zero (β i)] (h : κ → ι) (hh : Function.Injective h) :

DFinsupp.comapDomain h hh 0 = 0

@[simp]

theorem DFinsupp.comapDomain_add {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] {κ : Type u_1} [(i : ι) → AddZeroClass (β i)] (h : κ → ι) (hh : Function.Injective h) (f : Π₀ (i : ι), β i) (g : Π₀ (i : ι), β i) :

DFinsupp.comapDomain h hh (f + g) = DFinsupp.comapDomain h hh f + DFinsupp.comapDomain h hh g

@[simp]

theorem DFinsupp.comapDomain_smul {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] {κ : Type u_1} [Monoid γ] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] (h : κ → ι) (hh : Function.Injective h) (r : γ) (f : Π₀ (i : ι), β i) :

DFinsupp.comapDomain h hh (r • f) = r • DFinsupp.comapDomain h hh f

@[simp]

theorem DFinsupp.comapDomain_single {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] {κ : Type u_1} [DecidableEq κ] [(i : ι) → Zero (β i)] (h : κ → ι) (hh : Function.Injective h) (k : κ) (x : β (h k)) :

DFinsupp.comapDomain h hh (DFinsupp.single (h k) x) = DFinsupp.single k x

def DFinsupp.comapDomain' {ι : Type u} {β : ι → Type v} {κ : Type u_1} [(i : ι) → Zero (β i)] (h : κ → ι) {h' : ι → κ} (hh' : Function.LeftInverse h' h) (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.

@[simp]

theorem DFinsupp.comapDomain'_apply {ι : Type u} {β : ι → Type v} {κ : Type u_1} [(i : ι) → Zero (β i)] (h : κ → ι) {h' : ι → κ} (hh' : Function.LeftInverse h' h) (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' : Function.LeftInverse h' h) :

DFinsupp.comapDomain' h hh' 0 = 0

@[simp]

theorem DFinsupp.comapDomain'_add {ι : Type u} {β : ι → Type v} {κ : Type u_1} [(i : ι) → AddZeroClass (β i)] (h : κ → ι) {h' : ι → κ} (hh' : Function.LeftInverse h' h) (f : Π₀ (i : ι), β i) (g : Π₀ (i : ι), β i) :

DFinsupp.comapDomain' h hh' (f + g) = DFinsupp.comapDomain' h hh' f + DFinsupp.comapDomain' h hh' g

@[simp]

theorem DFinsupp.comapDomain'_smul {ι : Type u} {γ : Type w} {β : ι → Type v} {κ : Type u_1} [Monoid γ] [(i : ι) → AddMonoid (β i)] [(i : ι) → DistribMulAction γ (β i)] (h : κ → ι) {h' : ι → κ} (hh' : Function.LeftInverse h' h) (r : γ) (f : Π₀ (i : ι), β i) :

DFinsupp.comapDomain' h hh' (r • f) = r • DFinsupp.comapDomain' h hh' f

@[simp]

theorem DFinsupp.comapDomain'_single {ι : Type u} {β : ι → Type v} {κ : Type u_1} [DecidableEq ι] [DecidableEq κ] [(i : ι) → Zero (β i)] (h : κ → ι) {h' : ι → κ} (hh' : Function.LeftInverse h' h) (k : κ) (x : β (h k)) :

DFinsupp.comapDomain' h hh' (DFinsupp.single (h k) x) = DFinsupp.single k x

@[simp]

theorem DFinsupp.equivCongrLeft_apply {ι : Type u} {β : ι → Type v} {κ : Type u_1} [(i : ι) → Zero (β i)] (h : ι ≃ κ) (f : Π₀ (i : ι), β i) :

(DFinsupp.equivCongrLeft h) f = 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.

instance DFinsupp.hasAdd₂ {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type 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 : ι) → α i → Type 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 : ι) → α i → Type 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 : ι) → α i → Type v} [Monoid γ] [(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} [dec : DecidableEq ι] {α : ι → Type u_2} {δ : (i : ι) → α i → Type 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.

@[simp]

theorem DFinsupp.sigmaCurry_apply {ι : Type u} [dec : DecidableEq ι] {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → Zero (δ i j)] (f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd) (i : ι) (j : α i) :

((DFinsupp.sigmaCurry f) i) j = f { fst := i, snd := j }

@[simp]

theorem DFinsupp.sigmaCurry_zero {ι : Type u} [dec : DecidableEq ι] {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → Zero (δ i j)] :

DFinsupp.sigmaCurry 0 = 0

@[simp]

theorem DFinsupp.sigmaCurry_add {ι : Type u} [dec : DecidableEq ι] {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → AddZeroClass (δ i j)] (f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd) (g : Π₀ (i : (x : ι) × α x), δ i.fst i.snd) :

DFinsupp.sigmaCurry (f + g) = DFinsupp.sigmaCurry f + DFinsupp.sigmaCurry g

@[simp]

theorem DFinsupp.sigmaCurry_smul {ι : Type u} {γ : Type w} [dec : DecidableEq ι] {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [Monoid γ] [(i : ι) → (j : α i) → AddMonoid (δ i j)] [(i : ι) → (j : α i) → DistribMulAction γ (δ i j)] (r : γ) (f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd) :

DFinsupp.sigmaCurry (r • f) = r • DFinsupp.sigmaCurry f

@[simp]

theorem DFinsupp.sigmaCurry_single {ι : Type u} [dec : DecidableEq ι] {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → Zero (δ i j)] (ij : (i : ι) × α i) (x : δ ij.fst ij.snd) :

DFinsupp.sigmaCurry (DFinsupp.single ij x) = DFinsupp.single ij.fst (DFinsupp.single ij.snd x)

def DFinsupp.sigmaUncurry {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → Zero (δ i j)] [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)] (f : Π₀ (i : ι) (j : α i), δ i j) :

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

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

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem DFinsupp.sigmaUncurry_apply {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → Zero (δ i j)] [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)] (f : Π₀ (i : ι) (j : α i), δ i j) (i : ι) (j : α i) :

(DFinsupp.sigmaUncurry f) { fst := i, snd := j } = (f i) j

@[simp]

theorem DFinsupp.sigmaUncurry_zero {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → Zero (δ i j)] [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)] :

DFinsupp.sigmaUncurry 0 = 0

@[simp]

theorem DFinsupp.sigmaUncurry_add {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → AddZeroClass (δ i j)] [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)] (f : Π₀ (i : ι) (j : α i), δ i j) (g : Π₀ (i : ι) (j : α i), δ i j) :

DFinsupp.sigmaUncurry (f + g) = DFinsupp.sigmaUncurry f + DFinsupp.sigmaUncurry g

@[simp]

theorem DFinsupp.sigmaUncurry_smul {ι : Type u} {γ : Type w} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [Monoid γ] [(i : ι) → (j : α i) → AddMonoid (δ i j)] [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)] [(i : ι) → (j : α i) → DistribMulAction γ (δ i j)] (r : γ) (f : Π₀ (i : ι) (j : α i), δ i j) :

DFinsupp.sigmaUncurry (r • f) = r • DFinsupp.sigmaUncurry f

@[simp]

theorem DFinsupp.sigmaUncurry_single {ι : Type u} [dec : DecidableEq ι] {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → Zero (δ i j)] [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)] (i : ι) (j : α i) (x : δ i j) :

DFinsupp.sigmaUncurry (DFinsupp.single i (DFinsupp.single j x)) = DFinsupp.single { fst := i, snd := j } x

def DFinsupp.sigmaCurryEquiv {ι : Type u} [dec : DecidableEq ι] {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → Zero (δ i j)] [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)] :

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

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

This is the dfinsupp version of Equiv.piCurry.

Equations

DFinsupp.sigmaCurryEquiv = { toFun := DFinsupp.sigmaCurry, invFun := DFinsupp.sigmaUncurry, left_inv := ⋯, right_inv := ⋯ }

def DFinsupp.extendWith {ι : Type u} {α : Option ι → Type v} [(i : Option ι) → Zero (α i)] (a : α none) (f : Π₀ (i : ι), α (some i)) :

Π₀ (i : Option ι), α i

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

This is the dfinsupp version of Option.rec.

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem DFinsupp.extendWith_none {ι : Type u} {α : Option ι → Type v} [(i : Option ι) → Zero (α i)] (f : Π₀ (i : ι), α (some i)) (a : α none) :

(DFinsupp.extendWith a f) none = a

@[simp]

theorem DFinsupp.extendWith_some {ι : Type u} {α : Option ι → Type v} [(i : Option ι) → Zero (α i)] (f : Π₀ (i : ι), α (some i)) (a : α none) (i : ι) :

(DFinsupp.extendWith a f) (some i) = f i

@[simp]

theorem DFinsupp.extendWith_single_zero {ι : Type u} {α : Option ι → Type v} [DecidableEq ι] [(i : Option ι) → Zero (α i)] (i : ι) (x : α (some i)) :

DFinsupp.extendWith 0 (DFinsupp.single i x) = DFinsupp.single (some i) x

@[simp]

theorem DFinsupp.extendWith_zero {ι : Type u} {α : Option ι → Type v} [DecidableEq ι] [(i : Option ι) → Zero (α i)] (x : α none) :

DFinsupp.extendWith x 0 = DFinsupp.single none x

@[simp]

theorem DFinsupp.equivProdDFinsupp_apply {ι : Type u} [dec : DecidableEq ι] {α : Option ι → Type v} [(i : Option ι) → Zero (α i)] (f : Π₀ (i : Option ι), α i) :

DFinsupp.equivProdDFinsupp f = (f none, DFinsupp.comapDomain some ⋯ f)

@[simp]

theorem DFinsupp.equivProdDFinsupp_symm_apply {ι : Type u} [dec : DecidableEq ι] {α : Option ι → Type v} [(i : Option ι) → Zero (α i)] (f : α none × Π₀ (i : ι), α (some i)) :

DFinsupp.equivProdDFinsupp.symm f = DFinsupp.extendWith f.1 f.2

noncomputable def DFinsupp.equivProdDFinsupp {ι : Type u} [dec : DecidableEq ι] {α : Option ι → Type v} [(i : Option ι) → Zero (α i)] :

(Π₀ (i : Option ι), α 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.

theorem DFinsupp.equivProdDFinsupp_add {ι : Type u} [dec : DecidableEq ι] {α : Option ι → Type v} [(i : Option ι) → AddZeroClass (α i)] (f : Π₀ (i : Option ι), α i) (g : Π₀ (i : Option ι), α i) :

DFinsupp.equivProdDFinsupp (f + g) = DFinsupp.equivProdDFinsupp f + DFinsupp.equivProdDFinsupp g

theorem DFinsupp.equivProdDFinsupp_smul {ι : Type u} {γ : Type w} [dec : DecidableEq ι] {α : Option ι → Type v} [Monoid γ] [(i : Option ι) → AddMonoid (α i)] [(i : Option ι) → DistribMulAction γ (α i)] (r : γ) (f : Π₀ (i : Option ι), α i) :

DFinsupp.equivProdDFinsupp (r • f) = r • DFinsupp.equivProdDFinsupp f

def DFinsupp.sum {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → γ) :

γ

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

Equations

DFinsupp.sum f g = Finset.sum (DFinsupp.support f) fun (i : ι) => g i (f i)

def DFinsupp.prod {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommMonoid γ] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → γ) :

γ

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

Equations

DFinsupp.prod f g = Finset.prod (DFinsupp.support f) fun (i : ι) => g i (f i)

@[simp]

theorem map_dfinsupp_sum {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] {R : Type u_1} {S : Type u_2} {H : Type u_3} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid R] [AddCommMonoid S] [FunLike H R S] [AddMonoidHomClass H R S] (h : H) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R) :

h (DFinsupp.sum f g) = DFinsupp.sum f fun (a : ι) (b : β a) => h (g a b)

@[simp]

theorem map_dfinsupp_prod {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] {R : Type u_1} {S : Type u_2} {H : Type u_3} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommMonoid R] [CommMonoid S] [FunLike H R S] [MonoidHomClass H R S] (h : H) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R) :

h (DFinsupp.prod f g) = DFinsupp.prod f fun (a : ι) (b : β a) => h (g a b)

theorem DFinsupp.sum_mapRange_index {ι : Type u} {γ : Type w} [dec : DecidableEq ι] {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [(i : ι) → Zero (β₁ i)] [(i : ι) → Zero (β₂ i)] [(i : ι) → (x : β₁ i) → Decidable (x ≠ 0)] [(i : ι) → (x : β₂ i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {f : (i : ι) → β₁ i → β₂ i} {hf : ∀ (i : ι), f i 0 = 0} {g : Π₀ (i : ι), β₁ i} {h : (i : ι) → β₂ i → γ} (h0 : ∀ (i : ι), h i 0 = 0) :

DFinsupp.sum (DFinsupp.mapRange f hf g) h = DFinsupp.sum g fun (i : ι) (b : β₁ i) => h i (f i b)

theorem DFinsupp.prod_mapRange_index {ι : Type u} {γ : Type w} [dec : DecidableEq ι] {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [(i : ι) → Zero (β₁ i)] [(i : ι) → Zero (β₂ i)] [(i : ι) → (x : β₁ i) → Decidable (x ≠ 0)] [(i : ι) → (x : β₂ i) → Decidable (x ≠ 0)] [CommMonoid γ] {f : (i : ι) → β₁ i → β₂ i} {hf : ∀ (i : ι), f i 0 = 0} {g : Π₀ (i : ι), β₁ i} {h : (i : ι) → β₂ i → γ} (h0 : ∀ (i : ι), h i 0 = 1) :

DFinsupp.prod (DFinsupp.mapRange f hf g) h = DFinsupp.prod g fun (i : ι) (b : β₁ i) => h i (f i b)

theorem DFinsupp.sum_zero_index {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {h : (i : ι) → β i → γ} :

DFinsupp.sum 0 h = 0

theorem DFinsupp.prod_zero_index {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommMonoid γ] {h : (i : ι) → β i → γ} :

DFinsupp.prod 0 h = 1

theorem DFinsupp.sum_single_index {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {i : ι} {b : β i} {h : (i : ι) → β i → γ} (h_zero : h i 0 = 0) :

DFinsupp.sum (DFinsupp.single i b) h = h i b

theorem DFinsupp.prod_single_index {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommMonoid γ] {i : ι} {b : β i} {h : (i : ι) → β i → γ} (h_zero : h i 0 = 1) :

DFinsupp.prod (DFinsupp.single i b) h = h i b

theorem DFinsupp.sum_neg_index {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddGroup (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {g : Π₀ (i : ι), β i} {h : (i : ι) → β i → γ} (h0 : ∀ (i : ι), h i 0 = 0) :

DFinsupp.sum (-g) h = DFinsupp.sum g fun (i : ι) (b : β i) => h i (-b)

theorem DFinsupp.prod_neg_index {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddGroup (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommMonoid γ] {g : Π₀ (i : ι), β i} {h : (i : ι) → β i → γ} (h0 : ∀ (i : ι), h i 0 = 1) :

DFinsupp.prod (-g) h = DFinsupp.prod g 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} [DecidableEq ι₁] [DecidableEq ι₂] [(i : ι₁) → Zero (β₁ i)] [(i : ι₂) → Zero (β₂ i)] [(i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)] [(i : ι₂) → (x : β₂ i) → Decidable (x ≠ 0)] [AddCommMonoid γ] (f₁ : Π₀ (i : ι₁), β₁ i) (f₂ : Π₀ (i : ι₂), β₂ i) (h : (i : ι₁) → β₁ i → (i : ι₂) → β₂ i → γ) :

(DFinsupp.sum f₁ fun (i₁ : ι₁) (x₁ : β₁ i₁) => DFinsupp.sum f₂ fun (i₂ : ι₂) (x₂ : β₂ i₂) => h i₁ x₁ i₂ x₂) = DFinsupp.sum f₂ fun (i₂ : ι₂) (x₂ : β₂ i₂) => DFinsupp.sum f₁ 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} [DecidableEq ι₁] [DecidableEq ι₂] [(i : ι₁) → Zero (β₁ i)] [(i : ι₂) → Zero (β₂ i)] [(i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)] [(i : ι₂) → (x : β₂ i) → Decidable (x ≠ 0)] [CommMonoid γ] (f₁ : Π₀ (i : ι₁), β₁ i) (f₂ : Π₀ (i : ι₂), β₂ i) (h : (i : ι₁) → β₁ i → (i : ι₂) → β₂ i → γ) :

(DFinsupp.prod f₁ fun (i₁ : ι₁) (x₁ : β₁ i₁) => DFinsupp.prod f₂ fun (i₂ : ι₂) (x₂ : β₂ i₂) => h i₁ x₁ i₂ x₂) = DFinsupp.prod f₂ fun (i₂ : ι₂) (x₂ : β₂ i₂) => DFinsupp.prod f₁ fun (i₁ : ι₁) (x₁ : β₁ i₁) => h i₁ x₁ i₂ x₂

@[simp]

theorem DFinsupp.sum_apply {ι : Type u} {β : ι → Type v} {ι₁ : Type u₁} [DecidableEq ι₁] {β₁ : ι₁ → Type v₁} [(i₁ : ι₁) → Zero (β₁ i₁)] [(i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)] [(i : ι) → AddCommMonoid (β i)] {f : Π₀ (i₁ : ι₁), β₁ i₁} {g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i} {i₂ : ι} :

(DFinsupp.sum f g) i₂ = DFinsupp.sum f fun (i₁ : ι₁) (b : β₁ i₁) => (g i₁ b) i₂

theorem DFinsupp.support_sum {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] {ι₁ : Type u₁} [DecidableEq ι₁] {β₁ : ι₁ → 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} :

DFinsupp.support (DFinsupp.sum f g) ⊆ Finset.biUnion (DFinsupp.support f) fun (i : ι₁) => DFinsupp.support (g i (f i))

@[simp]

theorem DFinsupp.sum_zero {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {f : Π₀ (i : ι), β i} :

(DFinsupp.sum f fun (x : ι) (x : β x) => 0) = 0

@[simp]

theorem DFinsupp.prod_one {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommMonoid γ] {f : Π₀ (i : ι), β i} :

(DFinsupp.prod f fun (x : ι) (x : β x) => 1) = 1

@[simp]

theorem DFinsupp.sum_add {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {f : Π₀ (i : ι), β i} {h₁ : (i : ι) → β i → γ} {h₂ : (i : ι) → β i → γ} :

(DFinsupp.sum f fun (i : ι) (b : β i) => 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 : DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommMonoid γ] {f : Π₀ (i : ι), β i} {h₁ : (i : ι) → β i → γ} {h₂ : (i : ι) → β i → γ} :

(DFinsupp.prod f fun (i : ι) (b : β i) => h₁ i b * h₂ i b) = DFinsupp.prod f h₁ * DFinsupp.prod f h₂

@[simp]

theorem DFinsupp.sum_neg {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommGroup γ] {f : Π₀ (i : ι), β i} {h : (i : ι) → β i → γ} :

(DFinsupp.sum f fun (i : ι) (b : β i) => -h i b) = -DFinsupp.sum f h

@[simp]

theorem DFinsupp.prod_inv {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommGroup γ] {f : Π₀ (i : ι), β i} {h : (i : ι) → β i → γ} :

(DFinsupp.prod f fun (i : ι) (b : β i) => (h i b)⁻¹) = (DFinsupp.prod f h)⁻¹

theorem DFinsupp.sum_eq_zero {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {f : Π₀ (i : ι), β i} {h : (i : ι) → β i → γ} (hyp : ∀ (i : ι), h i (f i) = 0) :

DFinsupp.sum f h = 0

theorem DFinsupp.prod_eq_one {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommMonoid γ] {f : Π₀ (i : ι), β i} {h : (i : ι) → β i → γ} (hyp : ∀ (i : ι), h i (f i) = 1) :

DFinsupp.prod f h = 1

theorem DFinsupp.smul_sum {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] {α : Type u_1} [Monoid α] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] [DistribMulAction α γ] {f : Π₀ (i : ι), β i} {h : (i : ι) → β i → γ} {c : α} :

c • DFinsupp.sum f h = DFinsupp.sum f fun (a : ι) (b : β a) => c • h a b

theorem DFinsupp.sum_add_index {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {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₂) :

DFinsupp.sum (f + g) h = DFinsupp.sum f h + DFinsupp.sum g h

theorem DFinsupp.prod_add_index {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommMonoid γ] {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₂) :

DFinsupp.prod (f + g) h = DFinsupp.prod f h * DFinsupp.prod g h

theorem dfinsupp_sum_mem {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {S : Type u_1} [SetLike S γ] [AddSubmonoidClass S γ] (s : S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → γ) (h : ∀ (c : ι), f c ≠ 0 → g c (f c) ∈ s) :

DFinsupp.sum f g ∈ s

theorem dfinsupp_prod_mem {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommMonoid γ] {S : Type u_1} [SetLike S γ] [SubmonoidClass S γ] (s : S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → γ) (h : ∀ (c : ι), f c ≠ 0 → g c (f c) ∈ s) :

DFinsupp.prod f g ∈ s

@[simp]

theorem DFinsupp.sum_eq_sum_fintype {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] (v : Π₀ (i : ι), β i) {f : (i : ι) → β i → γ} (hf : ∀ (i : ι), f i 0 = 0) :

DFinsupp.sum v f = 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 : DecidableEq ι] [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommMonoid γ] (v : Π₀ (i : ι), β i) {f : (i : ι) → β i → γ} (hf : ∀ (i : ι), f i 0 = 1) :

DFinsupp.prod v f = Finset.prod Finset.univ fun (i : ι) => f i (DFinsupp.equivFunOnFintype v i)

@[simp]

theorem DFinsupp.prod_eq_zero_iff {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [CommMonoidWithZero γ] [Nontrivial γ] [NoZeroDivisors γ] [(i : ι) → DecidableEq (β i)] {f : Π₀ (i : ι), β i} {g : (i : ι) → β i → γ} :

DFinsupp.prod f g = 0 ↔ ∃ i ∈ DFinsupp.support f, g i (f i) = 0

theorem DFinsupp.prod_ne_zero_iff {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [CommMonoidWithZero γ] [Nontrivial γ] [NoZeroDivisors γ] [(i : ι) → DecidableEq (β i)] {f : Π₀ (i : ι), β i} {g : (i : ι) → β i → γ} :

DFinsupp.prod f g ≠ 0 ↔ ∀ i ∈ DFinsupp.support f, g i (f i) ≠ 0

def DFinsupp.sumAddHom {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] (φ : (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.

@[simp]

theorem DFinsupp.sumAddHom_single {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i) :

(DFinsupp.sumAddHom φ) (DFinsupp.single i x) = (φ i) x

@[simp]

theorem DFinsupp.sumAddHom_comp_single {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] (f : (i : ι) → β i →+ γ) (i : ι) :

AddMonoidHom.comp (DFinsupp.sumAddHom f) (DFinsupp.singleAddHom β i) = f i

theorem DFinsupp.sumAddHom_apply {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (f : Π₀ (i : ι), β i) :

(DFinsupp.sumAddHom φ) 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 : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] {S : Type u_1} [SetLike S γ] [AddSubmonoidClass S γ] (s : S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ γ) (h : ∀ (c : ι), f c ≠ 0 → (g c) (f c) ∈ s) :

(DFinsupp.sumAddHom g) f ∈ s

theorem AddSubmonoid.iSup_eq_mrange_dfinsupp_sumAddHom {ι : Type u} {γ : Type w} [dec : DecidableEq ι] [AddCommMonoid γ] (S : ι → AddSubmonoid γ) :

iSup S = AddMonoidHom.mrange (DFinsupp.sumAddHom fun (i : ι) => AddSubmonoid.subtype (S i))

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} [dec : DecidableEq ι] (p : ι → Prop) [DecidablePred p] [AddCommMonoid γ] (S : ι → AddSubmonoid γ) :

⨆ (i : ι), ⨆ (_ : p i), S i = AddMonoidHom.mrange (AddMonoidHom.comp (DFinsupp.sumAddHom fun (i : ι) => AddSubmonoid.subtype (S i)) (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} [dec : DecidableEq ι] [AddCommMonoid γ] (S : ι → AddSubmonoid γ) (x : γ) :

x ∈ iSup S ↔ ∃ (f : Π₀ (i : ι), ↥(S i)), (DFinsupp.sumAddHom fun (i : ι) => AddSubmonoid.subtype (S i)) f = x

theorem AddSubmonoid.mem_iSup_iff_exists_dfinsupp' {ι : Type u} {γ : Type w} [dec : DecidableEq ι] [AddCommMonoid γ] (S : ι → AddSubmonoid γ) [(i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)] (x : γ) :

x ∈ iSup S ↔ ∃ (f : Π₀ (i : ι), ↥(S i)), (DFinsupp.sum f 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} [dec : DecidableEq ι] (p : ι → Prop) [DecidablePred p] [AddCommMonoid γ] (S : ι → AddSubmonoid γ) (x : γ) :

x ∈ ⨆ (i : ι), ⨆ (_ : p i), S i ↔ ∃ (f : Π₀ (i : ι), ↥(S i)), (DFinsupp.sumAddHom fun (i : ι) => AddSubmonoid.subtype (S i)) (DFinsupp.filter p f) = x

theorem DFinsupp.sumAddHom_comm {ι₁ : Type u_4} {ι₂ : Type u_5} {β₁ : ι₁ → Type u_1} {β₂ : ι₂ → Type u_2} {γ : Type u_3} [DecidableEq ι₁] [DecidableEq ι₂] [(i : ι₁) → AddZeroClass (β₁ i)] [(i : ι₂) → AddZeroClass (β₂ i)] [AddCommMonoid γ] (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₂ : ι₂) => AddMonoidHom.flip (h i₁ i₂)) f₂) f₁

@[simp]

theorem DFinsupp.liftAddHom_symm_apply {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] (F : (Π₀ (i : ι), β i) →+ γ) (i : ι) :

(AddEquiv.symm DFinsupp.liftAddHom) F i = AddMonoidHom.comp F (DFinsupp.singleAddHom β i)

@[simp]

theorem DFinsupp.liftAddHom_apply {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) :

DFinsupp.liftAddHom φ = DFinsupp.sumAddHom φ

def DFinsupp.liftAddHom {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] :

((i : ι) → β i →+ γ) ≃+ ((Π₀ (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 : DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] :

DFinsupp.liftAddHom (DFinsupp.singleAddHom β) = AddMonoidHom.id (Π₀ (i : ι), β i)

The DFinsupp version of Finsupp.liftAddHom_singleAddHom,

theorem DFinsupp.liftAddHom_apply_single {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] (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} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] (f : (i : ι) → β i →+ γ) (i : ι) :

AddMonoidHom.comp (DFinsupp.liftAddHom f) (DFinsupp.singleAddHom β i) = f i

The DFinsupp version of Finsupp.liftAddHom_comp_single,

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

AddMonoidHom.comp g (DFinsupp.liftAddHom f) = DFinsupp.liftAddHom fun (a : ι) => AddMonoidHom.comp g (f a)

The DFinsupp version of Finsupp.comp_liftAddHom,

@[simp]

theorem DFinsupp.sumAddHom_zero {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] :

(DFinsupp.sumAddHom fun (i : ι) => 0) = 0

@[simp]

theorem DFinsupp.sumAddHom_add {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] (g : (i : ι) → β i →+ γ) (h : (i : ι) → β i →+ γ) :

(DFinsupp.sumAddHom fun (i : ι) => g i + h i) = DFinsupp.sumAddHom g + DFinsupp.sumAddHom h

@[simp]

theorem DFinsupp.sumAddHom_singleAddHom {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] :

DFinsupp.sumAddHom (DFinsupp.singleAddHom β) = AddMonoidHom.id (Π₀ (i : ι), β i)

theorem DFinsupp.comp_sumAddHom {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] {δ : Type u_1} [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] [AddCommMonoid δ] (g : γ →+ δ) (f : (i : ι) → β i →+ γ) :

AddMonoidHom.comp g (DFinsupp.sumAddHom f) = DFinsupp.sumAddHom fun (a : ι) => AddMonoidHom.comp g (f a)

theorem DFinsupp.sum_sub_index {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddGroup (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommGroup γ] {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₂) :

DFinsupp.sum (f - g) h = DFinsupp.sum f h - DFinsupp.sum g h

theorem DFinsupp.sum_finset_sum_index {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] {γ : Type w} {α : Type x} [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {s : Finset α} {g : α → Π₀ (i : ι), β i} {h : (i : ι) → β i → γ} (h_zero : ∀ (i : ι), h i 0 = 0) (h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ + h i b₂) :

(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 : DecidableEq ι] {γ : Type w} {α : Type x} [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommMonoid γ] {s : Finset α} {g : α → Π₀ (i : ι), β i} {h : (i : ι) → β i → γ} (h_zero : ∀ (i : ι), h i 0 = 1) (h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂) :

(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 : DecidableEq ι] {ι₁ : Type u₁} [DecidableEq ι₁] {β₁ : ι₁ → Type v₁} [(i₁ : ι₁) → Zero (β₁ i₁)] [(i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {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₂) :

DFinsupp.sum (DFinsupp.sum f g) h = DFinsupp.sum f fun (i : ι₁) (b : β₁ i) => DFinsupp.sum (g i b) h

theorem DFinsupp.prod_sum_index {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] {ι₁ : Type u₁} [DecidableEq ι₁] {β₁ : ι₁ → Type v₁} [(i₁ : ι₁) → Zero (β₁ i₁)] [(i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommMonoid γ] {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₂) :

DFinsupp.prod (DFinsupp.sum f g) h = DFinsupp.prod f fun (i : ι₁) (b : β₁ i) => DFinsupp.prod (g i b) h

@[simp]

theorem DFinsupp.sum_single {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), β i} :

DFinsupp.sum f DFinsupp.single = f

theorem DFinsupp.sum_subtypeDomain_index {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {v : Π₀ (i : ι), β i} {p : ι → Prop} [DecidablePred p] {h : (i : ι) → β i → γ} (hp : ∀ x ∈ DFinsupp.support v, p x) :

(DFinsupp.sum (DFinsupp.subtypeDomain p v) fun (i : Subtype p) (b : β ↑i) => h (↑i) b) = DFinsupp.sum v h

theorem DFinsupp.prod_subtypeDomain_index {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommMonoid γ] {v : Π₀ (i : ι), β i} {p : ι → Prop} [DecidablePred p] {h : (i : ι) → β i → γ} (hp : ∀ x ∈ DFinsupp.support v, p x) :

(DFinsupp.prod (DFinsupp.subtypeDomain p v) fun (i : Subtype p) (b : β ↑i) => h (↑i) b) = DFinsupp.prod v h

theorem DFinsupp.subtypeDomain_sum {ι : Type u} {γ : Type w} {β : ι → Type v} [(i : ι) → AddCommMonoid (β i)] {s : Finset γ} {h : γ → Π₀ (i : ι), β i} {p : ι → Prop} [DecidablePred p] :

DFinsupp.subtypeDomain p (Finset.sum s fun (c : γ) => h c) = Finset.sum s fun (c : γ) => DFinsupp.subtypeDomain p (h c)

theorem DFinsupp.subtypeDomain_finsupp_sum {ι : Type u} {γ : Type w} {β : ι → Type v} {δ : γ → Type x} [DecidableEq γ] [(c : γ) → Zero (δ c)] [(c : γ) → (x : δ c) → Decidable (x ≠ 0)] [(i : ι) → AddCommMonoid (β i)] {p : ι → Prop} [DecidablePred p] {s : Π₀ (c : γ), δ c} {h : (c : γ) → δ c → Π₀ (i : ι), β i} :

DFinsupp.subtypeDomain p (DFinsupp.sum s h) = DFinsupp.sum s 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.addMonoidHom f) x = 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

DFinsupp.mapRange.addMonoidHom f = { toZeroHom := { toFun := DFinsupp.mapRange (fun (i : ι) (x : β₁ i) => (f i) x) ⋯, map_zero' := ⋯ }, map_add' := ⋯ }

@[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 : ι) => AddMonoidHom.comp (f i) (f₂ i)) = AddMonoidHom.comp (DFinsupp.mapRange.addMonoidHom f) (DFinsupp.mapRange.addMonoidHom f₂)

@[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.addEquiv e) x = 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.

@[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 : ι) => AddEquiv.trans (f i) (f₂ i)) = AddEquiv.trans (DFinsupp.mapRange.addEquiv f) (DFinsupp.mapRange.addEquiv f₂)

@[simp]

theorem DFinsupp.mapRange.addEquiv_symm {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [(i : ι) → AddZeroClass (β₁ i)] [(i : ι) → AddZeroClass (β₂ i)] (e : (i : ι) → β₁ i ≃+ β₂ i) :

AddEquiv.symm (DFinsupp.mapRange.addEquiv e) = DFinsupp.mapRange.addEquiv fun (i : ι) => AddEquiv.symm (e 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.coe_dfinsupp_sum {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddMonoid R] [AddCommMonoid S] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R →+ S) :

⇑(DFinsupp.sum f g) = DFinsupp.sum f fun (a : ι) (b : β a) => ⇑(g a b)

@[simp]

theorem MonoidHom.coe_dfinsupp_prod {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [Monoid R] [CommMonoid S] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R →* S) :

⇑(DFinsupp.prod f g) = DFinsupp.prod f fun (a : ι) (b : β a) => ⇑(g a b)

theorem AddMonoidHom.dfinsupp_sum_apply {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddMonoid R] [AddCommMonoid S] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R →+ S) (r : R) :

(DFinsupp.sum f g) r = DFinsupp.sum f fun (a : ι) (b : β a) => (g a b) r

theorem MonoidHom.dfinsupp_prod_apply {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [Monoid R] [CommMonoid S] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R →* S) (r : R) :

(DFinsupp.prod f g) r = DFinsupp.prod f 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} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [AddCommMonoid R] [AddCommMonoid S] [(i : ι) → AddZeroClass (β i)] (h : R →+ S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ R) :

h ((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun (i : ι) => AddMonoidHom.comp h (g i)) f

theorem AddMonoidHom.dfinsupp_sumAddHom_apply {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [AddZeroClass R] [AddCommMonoid S] [(i : ι) → AddZeroClass (β i)] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ R →+ S) (r : R) :

((DFinsupp.sumAddHom g) f) r = (DFinsupp.sumAddHom fun (i : ι) => AddMonoidHom.comp (AddMonoidHom.eval r) (g i)) f

@[simp]

theorem AddMonoidHom.coe_dfinsupp_sumAddHom {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [AddZeroClass R] [AddCommMonoid S] [(i : ι) → AddZeroClass (β i)] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ R →+ S) :

⇑((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun (i : ι) => AddMonoidHom.comp (AddMonoidHom.coeFn R S) (g i)) f

@[simp]

theorem RingHom.map_dfinsupp_sumAddHom {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [NonAssocSemiring S] [(i : ι) → AddZeroClass (β i)] (h : R →+* S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ R) :

h ((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun (i : ι) => AddMonoidHom.comp (RingHom.toAddMonoidHom h) (g i)) f

@[simp]

theorem AddEquiv.map_dfinsupp_sumAddHom {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [AddCommMonoid R] [AddCommMonoid S] [(i : ι) → AddZeroClass (β i)] (h : R ≃+ S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ R) :

h ((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun (i : ι) => AddMonoidHom.comp (AddEquiv.toAddMonoidHom h) (g i)) f

instance DFinsupp.fintype {ι : Type u_1} {π : ι → Type u_2} [DecidableEq ι] [(i : ι) → Zero (π i)] [Fintype ι] [(i : ι) → Fintype (π i)] :

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

Equations

DFinsupp.fintype = Fintype.ofEquiv ((i : ι) → π i) DFinsupp.equivFunOnFintype.symm

instance DFinsupp.infinite_of_left {ι : Type u_1} {π : ι → Type u_2} [∀ (i : ι), Nontrivial (π i)] [(i : ι) → Zero (π i)] [Infinite ι] :

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

Equations

⋯ = ⋯

theorem DFinsupp.infinite_of_exists_right {ι : Type u_1} {π : ι → Type u_2} (i : ι) [Infinite (π i)] [(i : ι) → Zero (π i)] :

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

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

instance DFinsupp.infinite_of_right {ι : Type u_1} {π : ι → Type u_2} [∀ (i : ι), Infinite (π i)] [(i : ι) → Zero (π i)] [Nonempty ι] :

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

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

Equations

⋯ = ⋯