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)

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

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

• support' : Trunc { s_1 // ∀ (i : ι), i ∈ s_1 ∨ DFinsupp.toFun s i = 0 }

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

• )

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.

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Π₀_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

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

Equations

• DFinsupp.funLike = { coe := fun f => f.toFun, coe_injective' := (_ : ∀ (x x_1 : Π₀ (i : ι), β i), (fun f => f.toFun) x = (fun f => f.toFun) x_1 → x = x_1) }

instance DFinsupp.instCoeFunDFinsuppForAll {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] : CoeFun (Π₀ (i : ι), β i) fun x => (i : ι) → β i

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

Equations

• DFinsupp.instCoeFunDFinsuppForAll = inferInstance

@[simp]

theorem DFinsupp.toFun_eq_coe {ι : Type u} {β : ι → Type v} [(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 FunLike.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

@[deprecated FunLike.coe_injective]

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

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

Equations

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

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 // ∀ (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) (_ : ∀ (i : ι), id 0 = id 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 => if i ∈ s then x else y) (_ : ∀ (x : ι), (if x ∈ s then 0 else 0) = 0) 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_1 + x_2) (_ : ∀ (x : ι), 0 + 0 = 0) }

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 => ↑f) (_ : Function.Injective fun f => ↑f) (_ : ↑0 = 0) (_ : ∀ (g₁ g₂ : Π₀ (i : ι), β i), ↑(g₁ + g₂) = ↑g₁ + ↑g₂)

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 => DFinsupp.mapRange (fun x => (fun x_1 x_2 => x_1 • x_2) c) (_ : ∀ (x : ι), c • 0 = 0) v }

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

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

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 := FunLike.coe, map_zero' := (_ : ↑0 = 0) }, map_add' := (_ : ∀ (g₁ g₂ : Π₀ (i : ι), β i), ↑(g₁ + g₂) = ↑g₁ + ↑g₂) }

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

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

@[simp]

theorem DFinsupp.coe_finset_sum {ι : Type u} {β : ι → Type v} {α : Type u_1} [(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 => DFinsupp.mapRange (fun x => Neg.neg) (_ : ∀ (x : ι), -0 = 0) 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) (_ : ∀ (x : ι), 0 - 0 = 0) }

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 => DFinsupp.mapRange (fun x => (fun x_1 x_2 => x_1 • x_2) c) (_ : ∀ (x : ι), c • 0 = 0) v }

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

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

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

Equations

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

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 => DFinsupp.mapRange (fun x => (fun x_1 x_2 => x_1 • x_2) c) (_ : ∀ (x : ι), c • 0 = 0) v }

theorem DFinsupp.smul_apply {ι : Type u} {γ : Type w} {β : ι → Type v} [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

• @DFinsupp.smulCommClass = @DFinsupp.smulCommClass.proof_1

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

• @DFinsupp.isScalarTower = @DFinsupp.isScalarTower.proof_1

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

• @DFinsupp.isCentralScalar = @DFinsupp.isCentralScalar.proof_1

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 (_ : Function.Injective fun f => ↑f) (_ : ∀ (b : γ) (v : Π₀ (i : ι), β i), ↑(b • v) = b • ↑v)

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

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

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

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

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

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

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

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

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

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

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

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

@[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 (_ : Function.Injective fun f => ↑f)

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

Equations

• DFinsupp.uniqueOfIsEmpty = Function.Injective.unique (_ : Function.Injective fun f => ↑f)

@[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 := (_ : ∀ (j : ι), j ∈ {i} ∨ Pi.single i b j = 0) } }

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

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 x_1 => x ≠ x_1) i) 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

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

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

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

@[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}\beta_i$ to $\prod_{\mathtt{i : \iota}}\beta_i.$

Equations

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

@[simp]

theorem DFinsupp.mk_smul {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : 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) : Finset ι

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 => ↑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 // DFinsupp.support f = s }) (i : { x // x ∈ s }), ↑(↑(DFinsupp.subtypeSupportEqEquiv s) x i) = ↑↑x ↑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 // x ≠ 0 }) : ↑(↑(DFinsupp.subtypeSupportEqEquiv s).symm f) = DFinsupp.mk s fun i => ↑(f i)

def DFinsupp.subtypeSupportEqEquiv {ι : Type u} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (s : Finset ι) : { f // DFinsupp.support f = s } ≃ ((i : { x // x ∈ s }) → { x // 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_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

@[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 }), ↑(Sigma.snd (↑DFinsupp.sigmaFinsetFunEquiv a) i) = ↑a ↑i

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 // 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 = ∅) (_ : DFinsupp.support x = ∅ ↔ 0 = 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 : ι), ¬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 => 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 => 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 => ↑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 => ↑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 => ↑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

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

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 (_ : Function.RightInverse h.invFun h.toFun) 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

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

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 (_ : Function.Injective 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.fst f.snd

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] [AddMonoidHomClass H R S] (h : H) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R) : ↑h (DFinsupp.sum f g) = DFinsupp.sum f fun a b => ↑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] [MonoidHomClass H R S] (h : H) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R) : ↑h (DFinsupp.prod f g) = DFinsupp.prod f fun a b => ↑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 => 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 => 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 => 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 => 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₁ => DFinsupp.sum f₂ fun i₂ x₂ => h i₁ x₁ i₂ x₂) = DFinsupp.sum f₂ fun i₂ x₂ => DFinsupp.sum f₁ fun i₁ x₁ => h i₁ x₁ i₂ x₂

theorem DFinsupp.prod_comm {γ : Type w} {ι₁ : Type u_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₁ => DFinsupp.prod f₂ fun i₂ x₂ => h i₁ x₁ i₂ x₂) = DFinsupp.prod f₂ fun i₂ x₂ => DFinsupp.prod f₁ fun i₁ x₁ => h i₁ x₁ i₂ x₂

@[simp]

theorem DFinsupp.sum_apply {ι : Type u} {β : ι → Type v} {ι₁ : Type u₁} [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 => ↑(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 => 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 => 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 => 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 => 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 => -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 => (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 => 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)

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 : ι) (x : p i), S i = AddMonoidHom.mrange (AddMonoidHom.comp (DFinsupp.sumAddHom fun i => AddSubmonoid.subtype (S i)) (DFinsupp.filterAddMonoidHom (fun i => { x // x ∈ 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, ↑(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 : { x // x ∈ S i }) → Decidable (x ≠ 0)] (x : γ) : x ∈ iSup S ↔ ∃ f, (DFinsupp.sum f fun i xi => ↑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 : ι) (x : p i), S i ↔ ∃ f, ↑(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_apply {ι : Type u} {γ : Type w} {β : ι → Type v} [dec : DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) : ↑DFinsupp.liftAddHom φ = DFinsupp.sumAddHom φ

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

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 => 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 => 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 : ι) → x ∈ DFinsupp.support v → p x) : (DFinsupp.sum (DFinsupp.subtypeDomain p v) fun i b => h (↑i) b) = DFinsupp.sum v h

abbrev DFinsupp.sum_subtypeDomain_index.match_1 {ι : Type u_1} {p : ι → Prop} (motive : Subtype p → Prop) : (x : Subtype p) → ((a₁ : ι) → (ha₁ : p a₁) → motive { val := a₁, property := ha₁ }) → motive x

Equations

• DFinsupp.sum_subtypeDomain_index.match_1 motive x h_1 = Subtype.casesOn x fun val property => h_1 val property

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 : ι) → x ∈ DFinsupp.support v → p x) : (DFinsupp.prod (DFinsupp.subtypeDomain p v) fun i b => 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 => 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 => ↑(f i) x) (_ : ∀ (i : ι), ↑(f i) 0 = 0) 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

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

@[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 => ↑(e i) x) (_ : ∀ (i : ι), ↑(e i) 0 = 0) 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.

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 => ↑(g a b)

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 => ↑(g a b)

@[simp]

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 => ↑(g a b) r

@[simp]

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 => ↑(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

@[simp]

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

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

• @DFinsupp.infinite_of_left = @DFinsupp.infinite_of_left.proof_1

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

• @DFinsupp.infinite_of_right = @DFinsupp.infinite_of_right.proof_1