Dependent functions with finite support

For a non-dependent version see Mathlib/Data/Finsupp/Defs.lean.

Notation

This file introduces the notation Π₀ a, β a as notation for DFinsupp β, mirroring the α →₀ β notation used for Finsupp. This works for nested binders too, with Π₀ a b, γ a b as notation for DFinsupp (fun a ↦ DFinsupp (γ a)).

Implementation notes

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

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

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

structure DFinsupp {ι : Type u} (β : ι → Type v) [(i : ι) → Zero (β i)] : Type (max u v)

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

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

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

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

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

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

• )

def «termΠ₀_,_».«delab_app.DFinsupp» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

def «termΠ₀_,_» : Lean.ParserDescr

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

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

@[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 g : Π₀ (i : ι), β i} (h : ∀ (i : ι), f i = g i) : f = g

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

theorem DFinsupp.ne_iff {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] {f g : Π₀ (i : ι), β i} : f ≠ g ↔ ∃ (i : ι), f i ≠ g i

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

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

@[simp]

theorem DFinsupp.coe_mk' {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] (f : (i : ι) → β i) (s : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f i = 0 }) : ⇑{ toFun := f, support' := s } = f

@[simp]

theorem DFinsupp.coe_zero {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] : ⇑0 = 0

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

def DFinsupp.mapRange {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [(i : ι) → Zero (β₁ i)] [(i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ i → β₂ i) (hf : ∀ (i : ι), f i 0 = 0) (x : Π₀ (i : ι), β₁ i) : Π₀ (i : ι), β₂ i

The composition of f : β₁ → β₂ and g : Π₀ i, β₁ i is mapRange f hf g : Π₀ i, β₂ i, well defined when f 0 = 0.

This preserves the structure on f, and exists in various bundled forms for when f is itself bundled:

• DFinsupp.mapRange.addMonoidHom
• DFinsupp.mapRange.addEquiv
• dfinsupp.mapRange.linearMap
• dfinsupp.mapRange.linearEquiv

@[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 : ι) : (mapRange f hf g) i = f i (g i)

@[simp]

theorem DFinsupp.mapRange_id {ι : Type u} {β₁ : ι → Type v₁} [(i : ι) → Zero (β₁ i)] (h : ∀ (i : ι), id 0 = 0 := ⋯) (g : Π₀ (i : ι), β₁ i) : 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) : mapRange (fun (i : ι) => f i ∘ f₂ i) h g = mapRange f hf (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) : 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.

@[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 : ι) : (zipWith f hf g₁ g₂) i = f i (g₁ i) (g₂ i)

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

x.piecewise y s is the finitely supported function equal to x on the set s, and to y on its complement.

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

@[simp]

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

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

theorem DFinsupp.add_apply {ι : Type u} {β : ι → Type v} [(i : ι) → AddZeroClass (β i)] (g₁ g₂ : Π₀ (i : ι), β i) (i : ι) : (g₁ + g₂) i = g₁ i + g₂ i

@[simp]

theorem DFinsupp.coe_add {ι : Type u} {β : ι → Type v} [(i : ι) → AddZeroClass (β i)] (g₁ g₂ : Π₀ (i : ι), β i) : ⇑(g₁ + g₂) = ⇑g₁ + ⇑g₂

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

instance DFinsupp.instIsLeftCancelAdd {ι : Type u} {β : ι → Type v} [(i : ι) → AddZeroClass (β i)] [∀ (i : ι), IsLeftCancelAdd (β i)] : IsLeftCancelAdd (Π₀ (i : ι), β i)

instance DFinsupp.instIsRightCancelAdd {ι : Type u} {β : ι → Type v} [(i : ι) → AddZeroClass (β i)] [∀ (i : ι), IsRightCancelAdd (β i)] : IsRightCancelAdd (Π₀ (i : ι), β i)

instance DFinsupp.instIsCancelAdd {ι : Type u} {β : ι → Type v} [(i : ι) → AddZeroClass (β i)] [∀ (i : ι), IsCancelAdd (β i)] : IsCancelAdd (Π₀ (i : ι), β i)

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.

theorem DFinsupp.nsmul_apply {ι : Type u} {β : ι → Type v} [(i : ι) → AddMonoid (β i)] (b : ℕ) (v : Π₀ (i : ι), β i) (i : ι) : (b • v) i = b • v i

@[simp]

theorem DFinsupp.coe_nsmul {ι : Type u} {β : ι → Type v} [(i : ι) → AddMonoid (β i)] (b : ℕ) (v : Π₀ (i : ι), β i) : ⇑(b • v) = b • ⇑v

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

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.

@[simp]

theorem DFinsupp.coeFnAddMonoidHom_apply {ι : Type u} {β : ι → Type v} [(i : ι) → AddZeroClass (β i)] (v : Π₀ (i : ι), β i) : coeFnAddMonoidHom v = ⇑v

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

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

theorem DFinsupp.neg_apply {ι : Type u} {β : ι → Type v} [(i : ι) → AddGroup (β i)] (g : Π₀ (i : ι), β i) (i : ι) : (-g) i = -g i

@[simp]

theorem DFinsupp.coe_neg {ι : Type u} {β : ι → Type v} [(i : ι) → AddGroup (β i)] (g : Π₀ (i : ι), β i) : ⇑(-g) = -⇑g

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

theorem DFinsupp.sub_apply {ι : Type u} {β : ι → Type v} [(i : ι) → AddGroup (β i)] (g₁ g₂ : Π₀ (i : ι), β i) (i : ι) : (g₁ - g₂) i = g₁ i - g₂ i

@[simp]

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

theorem DFinsupp.zsmul_apply {ι : Type u} {β : ι → Type v} [(i : ι) → AddGroup (β i)] (b : ℤ) (v : Π₀ (i : ι), β i) (i : ι) : (b • v) i = b • v i

@[simp]

theorem DFinsupp.coe_zsmul {ι : Type u} {β : ι → Type v} [(i : ι) → AddGroup (β i)] (b : ℤ) (v : Π₀ (i : ι), β i) : ⇑(b • v) = b • ⇑v

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

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

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.

@[simp]

theorem DFinsupp.filter_apply {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] (p : ι → Prop) [DecidablePred p] (i : ι) (f : Π₀ (i : ι), β i) : (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) : (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) : (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] : filter p f + filter (fun (i : ι) => ¬p i) f = f

@[simp]

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

@[simp]

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

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

DFinsupp.filter as an AddMonoidHom.

@[simp]

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

@[simp]

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

@[simp]

theorem DFinsupp.filter_sub {ι : Type u} {β : ι → Type v} [(i : ι) → AddGroup (β i)] (p : ι → Prop) [DecidablePred p] (f g : Π₀ (i : ι), β i) : filter p (f - g) = filter p f - 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.

@[simp]

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

@[simp]

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

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.

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem DFinsupp.mk_apply {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [DecidableEq ι] {s : Finset ι} {x : (i : ↑↑s) → β ↑i} {i : ι} : (mk s x) i = if H : i ∈ s then x ⟨i, H⟩ else 0

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

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

@[deprecated DFinsupp.mk_of_notMem (since := "2025-05-23")]

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

Alias of DFinsupp.mk_of_notMem.

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

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

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

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.)

@[simp]

theorem DFinsupp.equivFunOnFintype_apply {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [Fintype ι] (a✝ : Π₀ (i : ι), β i) (a : ι) : equivFunOnFintype a✝ a = a✝ a

@[simp]

theorem DFinsupp.equivFunOnFintype_symm_coe {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [Fintype ι] (f : Π₀ (i : ι), β i) : equivFunOnFintype.symm ⇑f = f

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

The function single i b : Π₀ i, β i sends i to b and all other points to 0.

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

@[simp]

theorem DFinsupp.single_apply {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [DecidableEq ι] {i i' : ι} {b : β i} : (single i b) i' = if h : i = i' then Eq.recOn h b else 0

@[simp]

theorem DFinsupp.single_zero {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [DecidableEq ι] (i : ι) : single i 0 = 0

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

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

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

theorem DFinsupp.single_eq_single_iff {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [DecidableEq ι] (i j : ι) (xi : β i) (xj : β j) : single i xi = single j xj ↔ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Like Finsupp.single_eq_single_iff, but with a HEq due to dependent types

theorem DFinsupp.single_left_injective {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [DecidableEq ι] {b : (i : ι) → β i} (h : ∀ (i : ι), b i ≠ 0) : Function.Injective fun (i : ι) => single i (b i)

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

@[simp]

theorem DFinsupp.single_eq_zero {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [DecidableEq ι] {i : ι} {xi : β i} : single i xi = 0 ↔ xi = 0

theorem DFinsupp.single_ne_zero {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [DecidableEq ι] {i : ι} {xi : β i} : single i xi ≠ 0 ↔ xi ≠ 0

theorem DFinsupp.filter_single {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [DecidableEq ι] (p : ι → Prop) [DecidablePred p] (i : ι) (x : β i) : filter p (single i x) = if p i then single i x else 0

@[simp]

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

@[simp]

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

theorem DFinsupp.single_eq_of_sigma_eq {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [DecidableEq ι] {i j : ι} {xi : β i} {xj : β j} (h : ⟨i, xi⟩ = ⟨j, xj⟩) : single i xi = 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} [(i : ι) → Zero (β i)] [DecidableEq ι] [Fintype ι] (i : ι) (m : β i) : equivFunOnFintype (single i m) = Pi.single i m

@[simp]

theorem DFinsupp.equivFunOnFintype_symm_single {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [DecidableEq ι] [Fintype ι] (i : ι) (m : β i) : equivFunOnFintype.symm (Pi.single i m) = single i m

@[simp]

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

def DFinsupp.erase {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [DecidableEq ι] (i : ι) (x : Π₀ (i : ι), β i) : Π₀ (i : ι), β i

Redefine f i to be 0.

@[simp]

theorem DFinsupp.erase_apply {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [DecidableEq ι] {i j : ι} {f : Π₀ (i : ι), β i} : (erase i f) j = if j = i then 0 else f j

theorem DFinsupp.erase_same {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [DecidableEq ι] {i : ι} {f : Π₀ (i : ι), β i} : (erase i f) i = 0

theorem DFinsupp.erase_ne {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [DecidableEq ι] {i i' : ι} {f : Π₀ (i : ι), β i} (h : i' ≠ i) : (erase i f) i' = f i'

theorem DFinsupp.piecewise_single_erase {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [DecidableEq ι] (x : Π₀ (i : ι), β i) (i : ι) : (single i (x i)).piecewise (erase i x) {i} = x

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

@[simp]

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

@[simp]

theorem DFinsupp.filter_ne_eq_erase {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [DecidableEq ι] (f : Π₀ (i : ι), β i) (i : ι) : filter (fun (x : ι) => x ≠ i) f = erase i f

@[simp]

theorem DFinsupp.filter_ne_eq_erase' {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [DecidableEq ι] (f : Π₀ (i : ι), β i) (i : ι) : filter (fun (x : ι) => i ≠ x) f = erase i f

theorem DFinsupp.erase_single {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [DecidableEq ι] (j i : ι) (x : β i) : erase j (single i x) = if i = j then 0 else single i x

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

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

DFinsupp.single as an AddMonoidHom.

@[simp]

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

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

DFinsupp.erase as an AddMonoidHom.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem DFinsupp.induction {ι : Type u} {β : ι → Type v} [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 (single i b + f)) : p f

theorem DFinsupp.induction₂ {ι : Type u} {β : ι → Type v} [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 + single i b)) : p f

@[simp]

theorem DFinsupp.mk_add {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] {s : Finset ι} {x y : (i : ↑↑s) → β ↑i} : mk s (x + y) = mk s x + mk s y

@[simp]

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

@[simp]

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

@[simp]

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

def DFinsupp.mkAddGroupHom {ι : Type u} {β : ι → Type v} [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$.

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

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

@[simp]

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

@[simp]

theorem DFinsupp.support_mk'_subset {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : (i : ι) → β i} {s : Multiset ι} {h : ∀ (i : ι), i ∈ s ∨ f i = 0} : { toFun := f, support' := Trunc.mk ⟨s, h⟩ }.support ⊆ s.toFinset

@[simp]

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

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

def DFinsupp.subtypeSupportEqEquiv {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (s : Finset ι) : { f : Π₀ (i : ι), β i // f.support = s } ≃ ((i : { x : ι // x ∈ s }) → { x : β ↑i // x ≠ 0 })

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

@[simp]

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

@[simp]

theorem DFinsupp.subtypeSupportEqEquiv_apply_coe {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (s : Finset ι) (x✝ : { f : Π₀ (i : ι), β i // f.support = s }) (i : { x : ι // x ∈ s }) : ↑((subtypeSupportEqEquiv s) x✝ i) = ↑x✝ ↑i

def DFinsupp.sigmaFinsetFunEquiv {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] : (Π₀ (i : ι), β i) ≃ (s : Finset ι) × ((i : { x : ι // x ∈ s }) → { x : β ↑i // x ≠ 0 })

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

@[simp]

theorem DFinsupp.sigmaFinsetFunEquiv_apply_fst {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (a✝ : Π₀ (i : ι), β i) : (sigmaFinsetFunEquiv a✝).fst = a✝.support

@[simp]

theorem DFinsupp.sigmaFinsetFunEquiv_apply_snd_coe {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (a✝ : Π₀ (i : ι), β i) (i : { x : ι // x ∈ ((Equiv.sigmaFiberEquiv support).symm a✝).fst }) : ↑((sigmaFinsetFunEquiv a✝).snd i) = a✝ ↑i

@[simp]

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

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

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

@[deprecated DFinsupp.notMem_support_iff (since := "2025-05-23")]

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

Alias of DFinsupp.notMem_support_iff.

@[simp]

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

instance DFinsupp.decidableZero {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x = 0)] (f : Π₀ (i : ι), β i) : Decidable (f = 0)

theorem DFinsupp.support_subset_iff {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {s : Set ι} {f : Π₀ (i : ι), β i} : ↑f.support ⊆ s ↔ ∀ i ∉ s, f i = 0

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

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

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

@[simp]

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

theorem DFinsupp.mapRange_injective {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [(i : ι) → Zero (β₁ i)] [(i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ i → β₂ i) (hf : ∀ (i : ι), f i 0 = 0) : Function.Injective (mapRange f hf) ↔ ∀ (i : ι), Function.Injective (f i)

theorem DFinsupp.mapRange_surjective {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [(i : ι) → Zero (β₁ i)] [(i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ i → β₂ i) (hf : ∀ (i : ι), f i 0 = 0) : Function.Surjective (mapRange f hf) ↔ ∀ (i : ι), Function.Surjective (f i)

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

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} : zipWith f hf g₁ g₂ = mk (g₁.support ∪ g₂.support) fun (i : ↑↑(g₁.support ∪ g₂.support)) => f (↑i) (g₁ ↑i) (g₂ ↑i)

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

theorem DFinsupp.erase_def {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (i : ι) (f : Π₀ (i : ι), β i) : erase i f = mk (f.support.erase i) fun (j : ↑↑(f.support.erase i)) => f ↑j

@[simp]

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

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

theorem DFinsupp.support_update {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (f : Π₀ (i : ι), β i) (i : ι) (b : β i) [Decidable (b = 0)] : (f.update i b).support = if b = 0 then (erase i f).support else insert i f.support

theorem DFinsupp.filter_def {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {p : ι → Prop} [DecidablePred p] (f : Π₀ (i : ι), β i) : filter p f = mk (Finset.filter p f.support) fun (i : ↑↑(Finset.filter p f.support)) => f ↑i

@[simp]

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

theorem DFinsupp.subtypeDomain_def {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {p : ι → Prop} [DecidablePred p] (f : Π₀ (i : ι), β i) : subtypeDomain p f = mk (Finset.subtype p f.support) fun (i : ↑↑(Finset.subtype p f.support)) => f ↑↑i

@[simp]

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

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

@[simp]

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

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

noncomputable def DFinsupp.comapDomain {ι : Type u} {β : ι → Type v} {κ : 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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem DFinsupp.comapDomain_single {ι : Type u} {β : ι → Type v} {κ : Type u_1} [DecidableEq ι] [DecidableEq κ] [(i : ι) → Zero (β i)] (h : κ → ι) (hh : Function.Injective h) (k : κ) (x : β (h k)) : comapDomain h hh (single (h k) x) = 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.

@[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 : κ) : (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) : 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 g : Π₀ (i : ι), β i) : comapDomain' h hh' (f + g) = comapDomain' h hh' f + comapDomain' h hh' g

@[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)) : comapDomain' h hh' (single (h k) x) = single k x

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'.

@[simp]

theorem DFinsupp.equivCongrLeft_apply {ι : Type u} {β : ι → Type v} {κ : Type u_1} [(i : ι) → Zero (β i)] (h : ι ≃ κ) (f : Π₀ (i : ι), β i) : (equivCongrLeft h) f = comapDomain' ⇑h.symm ⋯ f

instance DFinsupp.hasAdd₂ {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → AddZeroClass (δ i j)] : Add (Π₀ (i : ι) (j : α i), δ i j)

instance DFinsupp.addZeroClass₂ {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → AddZeroClass (δ i j)] : AddZeroClass (Π₀ (i : ι) (j : α i), δ i j)

instance DFinsupp.addMonoid₂ {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → AddMonoid (δ i j)] : AddMonoid (Π₀ (i : ι) (j : α i), δ i j)

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.

@[simp]

theorem DFinsupp.extendWith_none {ι : Type u} {α : Option ι → Type v} [(i : Option ι) → Zero (α i)] (f : Π₀ (i : ι), α (some i)) (a : α none) : (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 : ι) : (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)) : extendWith 0 (single i x) = single (some i) x

@[simp]

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

noncomputable def DFinsupp.equivProdDFinsupp {ι : Type u} {α : 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.

@[simp]

theorem DFinsupp.equivProdDFinsupp_apply {ι : Type u} {α : Option ι → Type v} [(i : Option ι) → Zero (α i)] (f : Π₀ (i : Option ι), α i) : equivProdDFinsupp f = (f none, comapDomain some ⋯ f)

@[simp]

theorem DFinsupp.equivProdDFinsupp_symm_apply {ι : Type u} {α : Option ι → Type v} [(i : Option ι) → Zero (α i)] (f : α none × Π₀ (i : ι), α (some i)) : equivProdDFinsupp.symm f = extendWith f.1 f.2

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

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₁ g₂ : Π₀ (i : ι), β₁ i) : mapRange f hf (g₁ + g₂) = mapRange f hf g₁ + mapRange f hf g₂

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.

@[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) : (addMonoidHom f) x = mapRange (fun (i : ι) (x : β₁ i) => (f i) x) ⋯ x

@[simp]

theorem DFinsupp.mapRange.addMonoidHom_id {ι : Type u} {β₂ : ι → Type v₂} [(i : ι) → AddZeroClass (β₂ i)] : (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) : (addMonoidHom fun (i : ι) => (f i).comp (f₂ i)) = (addMonoidHom f).comp (addMonoidHom f₂)

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.

@[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) : (addEquiv e) x = mapRange (fun (i : ι) (x : β₁ i) => (e i) x) ⋯ x

@[simp]

theorem DFinsupp.mapRange.addEquiv_refl {ι : Type u} {β₁ : ι → Type v₁} [(i : ι) → AddZeroClass (β₁ i)] : (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) : (addEquiv fun (i : ι) => (f i).trans (f₂ i)) = (addEquiv f).trans (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 e).symm = addEquiv fun (i : ι) => (e i).symm