Documentation

Mathlib.Data.DFinsupp.Defs

Dependent functions with finite support #

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

Notation #

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

Implementation notes #

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

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

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

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

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

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

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

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

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

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

  • )
Instances For

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

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

      Pretty printer defined by notation3 command.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        instance DFinsupp.instDFunLike {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] :
        DFunLike (Π₀ (i : ι), β i) ι β
        Equations
        • DFinsupp.instDFunLike = { coe := fun (f : Π₀ (i : ι), β i) => f.toFun, coe_injective' := }
        @[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.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)
        Equations
        • DFinsupp.instZero = { zero := { toFun := 0, support' := Trunc.mk , } }
        instance DFinsupp.instInhabited {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] :
        Inhabited (Π₀ (i : ι), β i)
        Equations
        • DFinsupp.instInhabited = { default := 0 }
        @[simp]
        theorem DFinsupp.coe_mk' {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] (f : (i : ι) → β i) (s : Trunc { s : 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:

        Equations
        Instances For
          @[simp]
          theorem DFinsupp.mapRange_apply {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → Zero (β₁ i)] [(i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ iβ₂ i) (hf : ∀ (i : ι), f i 0 = 0) (g : Π₀ (i : ι), β₁ i) (i : ι) :
          (DFinsupp.mapRange f hf g) i = f i (g i)
          @[simp]
          theorem DFinsupp.mapRange_id {ι : Type u} {β₁ : ιType v₁} [(i : ι) → Zero (β₁ i)] (h : ∀ (i : ι), id 0 = 0 := ) (g : Π₀ (i : ι), β₁ i) :
          DFinsupp.mapRange (fun (i : ι) => id) h g = g
          theorem DFinsupp.mapRange_comp {ι : Type u} {β : ιType v} {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → Zero (β i)] [(i : ι) → Zero (β₁ i)] [(i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ iβ₂ i) (f₂ : (i : ι) → β iβ₁ i) (hf : ∀ (i : ι), f i 0 = 0) (hf₂ : ∀ (i : ι), f₂ i 0 = 0) (h : ∀ (i : ι), (f i f₂ i) 0 = 0) (g : Π₀ (i : ι), β i) :
          DFinsupp.mapRange (fun (i : ι) => f i f₂ i) h g = DFinsupp.mapRange f hf (DFinsupp.mapRange f₂ hf₂ g)
          @[simp]
          theorem DFinsupp.mapRange_zero {ι : Type u} {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → Zero (β₁ i)] [(i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ iβ₂ i) (hf : ∀ (i : ι), f i 0 = 0) :
          def DFinsupp.zipWith {ι : Type u} {β : ιType v} {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → Zero (β i)] [(i : ι) → Zero (β₁ i)] [(i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ iβ₂ iβ i) (hf : ∀ (i : ι), f i 0 0 = 0) (x : Π₀ (i : ι), β₁ i) (y : Π₀ (i : ι), β₂ i) :
          Π₀ (i : ι), β i

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem DFinsupp.zipWith_apply {ι : Type u} {β : ιType v} {β₁ : ιType v₁} {β₂ : ιType v₂} [(i : ι) → Zero (β i)] [(i : ι) → Zero (β₁ i)] [(i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ iβ₂ iβ i) (hf : ∀ (i : ι), f i 0 0 = 0) (g₁ : Π₀ (i : ι), β₁ i) (g₂ : Π₀ (i : ι), β₂ i) (i : ι) :
            (DFinsupp.zipWith f hf g₁ g₂) i = f i (g₁ i) (g₂ i)
            def DFinsupp.piecewise {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] (x y : Π₀ (i : ι), β i) (s : Set ι) [(i : ι) → Decidable (i s)] :
            Π₀ (i : ι), β i

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

            Equations
            Instances For
              theorem DFinsupp.piecewise_apply {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] (x 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)
              Equations
              • DFinsupp.instAdd = { add := DFinsupp.zipWith (fun (x : ι) (x1 x2 : β x) => x1 + x2) }
              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)
              Equations
              instance DFinsupp.instIsLeftCancelAdd {ι : Type u} {β : ιType v} [(i : ι) → AddZeroClass (β i)] [∀ (i : ι), IsLeftCancelAdd (β i)] :
              IsLeftCancelAdd (Π₀ (i : ι), β i)
              Equations
              • =
              instance DFinsupp.instIsRightCancelAdd {ι : Type u} {β : ιType v} [(i : ι) → AddZeroClass (β i)] [∀ (i : ι), IsRightCancelAdd (β i)] :
              IsRightCancelAdd (Π₀ (i : ι), β i)
              Equations
              • =
              instance DFinsupp.instIsCancelAdd {ι : Type u} {β : ιType v} [(i : ι) → AddZeroClass (β i)] [∀ (i : ι), IsCancelAdd (β i)] :
              IsCancelAdd (Π₀ (i : ι), β i)
              Equations
              • =
              instance DFinsupp.hasNatScalar {ι : Type u} {β : ιType v} [(i : ι) → AddMonoid (β i)] :
              SMul (Π₀ (i : ι), β i)

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

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

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

              Equations
              • DFinsupp.coeFnAddMonoidHom = { toFun := DFunLike.coe, map_zero' := , map_add' := }
              Instances For
                instance DFinsupp.addCommMonoid {ι : Type u} {β : ιType v} [(i : ι) → AddCommMonoid (β i)] :
                AddCommMonoid (Π₀ (i : ι), β i)
                Equations
                instance DFinsupp.instNeg {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] :
                Neg (Π₀ (i : ι), β i)
                Equations
                • DFinsupp.instNeg = { neg := fun (f : Π₀ (i : ι), β i) => DFinsupp.mapRange (fun (x : ι) => Neg.neg) f }
                theorem DFinsupp.neg_apply {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] (g : Π₀ (i : ι), β i) (i : ι) :
                (-g) i = -g i
                @[simp]
                theorem DFinsupp.coe_neg {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] (g : Π₀ (i : ι), β i) :
                (-g) = -g
                instance DFinsupp.instSub {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] :
                Sub (Π₀ (i : ι), β i)
                Equations
                theorem DFinsupp.sub_apply {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] (g₁ 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.

                Equations
                • DFinsupp.hasIntScalar = { smul := fun (c : ) (v : Π₀ (i : ι), β i) => DFinsupp.mapRange (fun (x : ι) (x_1 : β x) => c x_1) v }
                theorem DFinsupp.zsmul_apply {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] (b : ) (v : Π₀ (i : ι), β i) (i : ι) :
                (b v) i = b v i
                @[simp]
                theorem DFinsupp.coe_zsmul {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] (b : ) (v : Π₀ (i : ι), β i) :
                (b v) = b v
                instance DFinsupp.instAddGroup {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] :
                AddGroup (Π₀ (i : ι), β i)
                Equations
                instance DFinsupp.addCommGroup {ι : Type u} {β : ιType v} [(i : ι) → AddCommGroup (β i)] :
                AddCommGroup (Π₀ (i : ι), β i)
                Equations
                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
                • DFinsupp.filter p x = { toFun := fun (i : ι) => if p i then x i else 0, support' := Trunc.map (fun (xs : { s : Multiset ι // ∀ (i : ι), i s x.toFun i = 0 }) => xs, ) x.support' }
                Instances For
                  @[simp]
                  theorem DFinsupp.filter_apply {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] (p : ιProp) [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] :
                  @[simp]
                  theorem DFinsupp.filter_add {ι : Type u} {β : ιType v} [(i : ι) → AddZeroClass (β i)] (p : ιProp) [DecidablePred p] (f g : Π₀ (i : ι), β i) :
                  def DFinsupp.filterAddMonoidHom {ι : Type u} (β : ιType v) [(i : ι) → AddZeroClass (β i)] (p : ιProp) [DecidablePred p] :
                  (Π₀ (i : ι), β i) →+ Π₀ (i : ι), β i

                  DFinsupp.filter as an AddMonoidHom.

                  Equations
                  Instances For
                    @[simp]
                    theorem DFinsupp.filterAddMonoidHom_apply {ι : Type u} (β : ιType v) [(i : ι) → AddZeroClass (β i)] (p : ιProp) [DecidablePred p] (x : Π₀ (i : ι), β i) :
                    @[simp]
                    theorem DFinsupp.filter_neg {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] (p : ιProp) [DecidablePred p] (f : Π₀ (i : ι), β i) :
                    @[simp]
                    theorem DFinsupp.filter_sub {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] (p : ιProp) [DecidablePred p] (f g : Π₀ (i : ι), β i) :
                    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.
                    Instances For
                      @[simp]
                      theorem DFinsupp.subtypeDomain_zero {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] {p : ιProp} [DecidablePred p] :
                      @[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 v' : Π₀ (i : ι), β i) :
                      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
                      Instances For
                        @[simp]
                        theorem DFinsupp.subtypeDomainAddMonoidHom_apply {ι : Type u} (β : ιType v) [(i : ι) → AddZeroClass (β i)] (p : ιProp) [DecidablePred p] (x : Π₀ (i : ι), β i) :
                        @[simp]
                        theorem DFinsupp.subtypeDomain_neg {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] {p : ιProp} [DecidablePred p] {v : Π₀ (i : ι), β i} :
                        @[simp]
                        theorem DFinsupp.subtypeDomain_sub {ι : Type u} {β : ιType v} [(i : ι) → AddGroup (β i)] {p : ιProp} [DecidablePred p] {v v' : Π₀ (i : ι), β i} :
                        theorem DFinsupp.finite_support {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] (f : Π₀ (i : ι), β i) :
                        {i : ι | f i 0}.Finite
                        def DFinsupp.mk {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [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.

                        Equations
                        • DFinsupp.mk s x = { toFun := fun (i : ι) => if H : i s then x i, H else 0, support' := Trunc.mk s.val, }
                        Instances For
                          @[simp]
                          theorem DFinsupp.mk_apply {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [DecidableEq ι] {s : Finset ι} {x : (i : s) → β i} {i : ι} :
                          (DFinsupp.mk s x) i = if H : i s then x i, H else 0
                          theorem DFinsupp.mk_of_mem {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [DecidableEq ι] {s : Finset ι} {x : (i : s) → β i} {i : ι} (hi : i s) :
                          (DFinsupp.mk s x) i = x i, hi
                          theorem DFinsupp.mk_of_not_mem {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [DecidableEq ι] {s : Finset ι} {x : (i : s) → β i} {i : ι} (hi : is) :
                          (DFinsupp.mk s x) i = 0
                          theorem DFinsupp.mk_injective {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [DecidableEq ι] (s : Finset ι) :
                          instance DFinsupp.unique {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [∀ (i : ι), Subsingleton (β i)] :
                          Unique (Π₀ (i : ι), β i)
                          Equations
                          • DFinsupp.unique = .unique
                          instance DFinsupp.uniqueOfIsEmpty {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [IsEmpty ι] :
                          Unique (Π₀ (i : ι), β i)
                          Equations
                          • DFinsupp.uniqueOfIsEmpty = .unique
                          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
                          • DFinsupp.equivFunOnFintype = { toFun := DFunLike.coe, invFun := fun (f : (i : ι) → β i) => { toFun := f, support' := Trunc.mk Finset.univ.val, }, left_inv := , right_inv := }
                          Instances For
                            @[simp]
                            theorem DFinsupp.equivFunOnFintype_apply {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [Fintype ι] (a✝ : Π₀ (i : ι), β i) (a : ι) :
                            DFinsupp.equivFunOnFintype a✝ a = a✝ a
                            @[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} [(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.

                            Equations
                            Instances For
                              theorem DFinsupp.single_eq_pi_single {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [DecidableEq ι] {i : ι} {b : β i} :
                              @[simp]
                              theorem DFinsupp.single_apply {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [DecidableEq ι] {i i' : ι} {b : β i} :
                              (DFinsupp.single i b) i' = if h : i = i' then Eq.recOn h b else 0
                              @[simp]
                              theorem DFinsupp.single_zero {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [DecidableEq ι] (i : ι) :
                              theorem DFinsupp.single_eq_same {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [DecidableEq ι] {i : ι} {b : β i} :
                              (DFinsupp.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') :
                              (DFinsupp.single i b) i' = 0
                              theorem DFinsupp.single_injective {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [DecidableEq ι] {i : ι} :
                              theorem DFinsupp.single_eq_single_iff {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [DecidableEq ι] (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} [(i : ι) → Zero (β i)] [DecidableEq ι] {b : (i : ι) → β i} (h : ∀ (i : ι), b i 0) :
                              Function.Injective fun (i : ι) => DFinsupp.single i (b i)

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

                              @[simp]
                              theorem DFinsupp.single_eq_zero {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [DecidableEq ι] {i : ι} {xi : β i} :
                              DFinsupp.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) :
                              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} [(i : ι) → Zero (β i)] [DecidableEq ι] {p : ιProp} [DecidablePred p] (i : ι) (x : β i) (h : p i) :
                              @[simp]
                              theorem DFinsupp.filter_single_neg {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [DecidableEq ι] {p : ιProp} [DecidablePred p] (i : ι) (x : β i) (h : ¬p i) :
                              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) :

                              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) :
                              DFinsupp.equivFunOnFintype (DFinsupp.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) :
                              DFinsupp.equivFunOnFintype.symm (Pi.single i m) = DFinsupp.single i m
                              @[simp]
                              theorem DFinsupp.zipWith_single_single {ι : Type u} {β : ιType v} {β₁ : ιType v₁} {β₂ : ιType v₂} [(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) :
                              DFinsupp.zipWith f hf (DFinsupp.single i b₁) (DFinsupp.single i b₂) = DFinsupp.single i (f i b₁ b₂)
                              def DFinsupp.erase {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [DecidableEq ι] (i : ι) (x : Π₀ (i : ι), β i) :
                              Π₀ (i : ι), β i

                              Redefine f i to be 0.

                              Equations
                              • DFinsupp.erase i x = { toFun := fun (j : ι) => if j = i then 0 else x.toFun j, support' := Trunc.map (fun (xs : { s : Multiset ι // ∀ (i : ι), i s x.toFun i = 0 }) => xs, ) x.support' }
                              Instances For
                                @[simp]
                                theorem DFinsupp.erase_apply {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [DecidableEq ι] {i j : ι} {f : Π₀ (i : ι), β i} :
                                (DFinsupp.erase i f) j = if j = i then 0 else f j
                                theorem DFinsupp.erase_same {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [DecidableEq ι] {i : ι} {f : Π₀ (i : ι), β i} :
                                (DFinsupp.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) :
                                (DFinsupp.erase i f) i' = f i'
                                theorem DFinsupp.piecewise_single_erase {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [DecidableEq ι] (x : Π₀ (i : ι), β i) (i : ι) [(i' : ι) → Decidable (i' {i})] :
                                (DFinsupp.single i (x i)).piecewise (DFinsupp.erase i x) {i} = x
                                theorem DFinsupp.erase_eq_sub_single {ι : Type u} [DecidableEq ι] {β : ιType u_1} [(i : ι) → AddGroup (β i)] (f : Π₀ (i : ι), β i) (i : ι) :
                                @[simp]
                                theorem DFinsupp.erase_zero {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [DecidableEq ι] (i : ι) :
                                @[simp]
                                theorem DFinsupp.filter_ne_eq_erase {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [DecidableEq ι] (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} [(i : ι) → Zero (β i)] [DecidableEq ι] (f : Π₀ (i : ι), β i) (i : ι) :
                                DFinsupp.filter (fun (x : ι) => i x) f = DFinsupp.erase i f
                                theorem DFinsupp.erase_single {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [DecidableEq ι] (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} [(i : ι) → Zero (β i)] [DecidableEq ι] (i : ι) (x : β i) :
                                @[simp]
                                theorem DFinsupp.erase_single_ne {ι : Type u} {β : ιType v} [(i : ι) → Zero (β i)] [DecidableEq ι] {i j : ι} (x : β i) (h : i j) :
                                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.

                                Equations
                                Instances For
                                  @[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 = DFinsupp.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 = DFinsupp.single i b + DFinsupp.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 = DFinsupp.erase i f + DFinsupp.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 - DFinsupp.single i (f i) + DFinsupp.single i b
                                  @[simp]
                                  theorem DFinsupp.single_add {ι : Type u} {β : ιType v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] (i : ι) (b₁ b₂ : β i) :
                                  DFinsupp.single i (b₁ + b₂) = DFinsupp.single i b₁ + DFinsupp.single i b₂
                                  @[simp]
                                  theorem DFinsupp.erase_add {ι : Type u} {β : ιType v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] (i : ι) (f₁ f₂ : Π₀ (i : ι), β i) :
                                  DFinsupp.erase i (f₁ + f₂) = DFinsupp.erase i f₁ + DFinsupp.erase i f₂
                                  def DFinsupp.singleAddHom {ι : Type u} (β : ιType v) [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] (i : ι) :
                                  β i →+ Π₀ (i : ι), β i

                                  DFinsupp.single as an AddMonoidHom.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem DFinsupp.singleAddHom_apply {ι : Type u} (β : ιType v) [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] (i : ι) (b : β i) :
                                    def DFinsupp.eraseAddHom {ι : Type u} (β : ιType v) [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] (i : ι) :
                                    (Π₀ (i : ι), β i) →+ Π₀ (i : ι), β i

                                    DFinsupp.erase as an AddMonoidHom.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem DFinsupp.eraseAddHom_apply {ι : Type u} (β : ιType v) [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] (i : ι) (x : Π₀ (i : ι), β i) :
                                      @[simp]
                                      theorem DFinsupp.single_neg {ι : Type u} [DecidableEq ι] {β : ιType v} [(i : ι) → AddGroup (β i)] (i : ι) (x : β i) :
                                      @[simp]
                                      theorem DFinsupp.single_sub {ι : Type u} [DecidableEq ι] {β : ιType v} [(i : ι) → AddGroup (β i)] (i : ι) (x y : β i) :
                                      @[simp]
                                      theorem DFinsupp.erase_neg {ι : Type u} [DecidableEq ι] {β : ιType v} [(i : ι) → AddGroup (β i)] (i : ι) (f : Π₀ (i : ι), β i) :
                                      @[simp]
                                      theorem DFinsupp.erase_sub {ι : Type u} [DecidableEq ι] {β : ιType v} [(i : ι) → AddGroup (β i)] (i : ι) (f g : Π₀ (i : ι), β i) :
                                      theorem DFinsupp.single_add_erase {ι : Type u} {β : ιType v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] (i : ι) (f : Π₀ (i : ι), β i) :
                                      theorem DFinsupp.erase_add_single {ι : Type u} {β : ιType v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] (i : ι) (f : Π₀ (i : ι), β i) :
                                      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 = 0b 0p fp (DFinsupp.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 = 0b 0p fp (f + DFinsupp.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} :
                                      @[simp]
                                      theorem DFinsupp.mk_zero {ι : Type u} {β : ιType v} [DecidableEq ι] [(i : ι) → Zero (β i)] {s : Finset ι} :
                                      @[simp]
                                      theorem DFinsupp.mk_neg {ι : Type u} {β : ιType v} [DecidableEq ι] [(i : ι) → AddGroup (β i)] {s : Finset ι} {x : (i : s) → β i} :
                                      @[simp]
                                      theorem DFinsupp.mk_sub {ι : Type u} {β : ιType v} [DecidableEq ι] [(i : ι) → AddGroup (β i)] {s : Finset ι} {x y : (i : s) → β i} :
                                      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.$

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

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

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[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} :
                                          (DFinsupp.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 = DFinsupp.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}.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[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 }) :
                                            ((DFinsupp.subtypeSupportEqEquiv s).symm f) = DFinsupp.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 }) :
                                            ((DFinsupp.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}⟩.

                                            Equations
                                            Instances For
                                              @[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 DFinsupp.support).symm a✝).fst }) :
                                              ((DFinsupp.sigmaFinsetFunEquiv a✝).snd i) = a✝ i
                                              @[simp]
                                              theorem DFinsupp.sigmaFinsetFunEquiv_apply_fst {ι : Type u} {β : ιType v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] (a✝ : Π₀ (i : ι), β i) :
                                              (DFinsupp.sigmaFinsetFunEquiv a✝).fst = a✝.support
                                              @[simp]
                                              theorem DFinsupp.support_zero {ι : Type u} {β : ιType v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 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.not_mem_support_iff {ι : Type u} {β : ιType v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] {f : Π₀ (i : ι), β i} {i : ι} :
                                              if.support f i = 0
                                              @[simp]
                                              theorem DFinsupp.support_eq_empty {ι : Type u} {β : ιType v} [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)
                                              Equations
                                              • f.decidableZero = f.support'.recOnSubsingleton fun (s : { s : Multiset ι // ∀ (i : ι), i s f.toFun i = 0 }) => decidable_of_iff (∀ is, f i = 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 is, 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) :
                                              (DFinsupp.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} :
                                              (DFinsupp.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} :
                                              DFinsupp.mapRange f hf g = DFinsupp.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} :
                                              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} :
                                              (DFinsupp.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} :
                                              DFinsupp.zipWith f hf g₁ g₂ = DFinsupp.mk (g₁.support g₂.support) fun (i : (g₁.support g₂.support)) => f (↑i) (g₁ i) (g₂ i)
                                              theorem DFinsupp.support_zipWith {ι : Type u} {β : ιType v} {β₁ : ιType v₁} {β₂ : ιType v₂} [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.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) :
                                              DFinsupp.erase i f = DFinsupp.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) :
                                              (DFinsupp.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 (DFinsupp.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) :
                                              DFinsupp.filter p f = DFinsupp.mk (Finset.filter p f.support) fun (i : (Finset.filter p f.support)) => f i
                                              @[simp]
                                              theorem DFinsupp.support_filter {ι : Type u} {β : ιType v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] {p : ιProp} [DecidablePred p] (f : Π₀ (i : ι), β i) :
                                              (DFinsupp.filter p f).support = Finset.filter (fun (x : ι) => p x) f.support
                                              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) :
                                              DFinsupp.subtypeDomain p f = DFinsupp.mk (Finset.subtype p f.support) fun (i : (Finset.subtype p f.support)) => f i
                                              @[simp]
                                              theorem DFinsupp.support_subtypeDomain {ι : Type u} {β : ιType v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x 0)] {p : ιProp} [DecidablePred p] {f : Π₀ (i : ι), β i} :
                                              (DFinsupp.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)
                                              Equations
                                              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.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[simp]
                                                theorem DFinsupp.comapDomain_apply {ι : Type u} {β : ιType v} {κ : Type u_1} [(i : ι) → Zero (β i)] (h : κι) (hh : 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} {κ : Type u_1} [(i : ι) → Zero (β i)] (h : κι) (hh : Function.Injective h) :
                                                @[simp]
                                                theorem DFinsupp.comapDomain_add {ι : Type u} {β : ιType v} {κ : Type u_1} [(i : ι) → AddZeroClass (β i)] (h : κι) (hh : Function.Injective h) (f g : Π₀ (i : ι), β i) :
                                                @[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)) :
                                                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.
                                                Instances For
                                                  @[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) :
                                                  @[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) :
                                                  @[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)) :
                                                  def DFinsupp.equivCongrLeft {ι : Type u} {β : ιType v} {κ : Type u_1} [(i : ι) → Zero (β i)] (h : ι κ) :
                                                  (Π₀ (i : ι), β i) Π₀ (k : κ), β (h.symm k)

                                                  Reindexing terms of a dfinsupp.

                                                  This is the dfinsupp version of Equiv.piCongrLeft'.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[simp]
                                                    theorem DFinsupp.equivCongrLeft_apply {ι : Type u} {β : ιType v} {κ : Type u_1} [(i : ι) → Zero (β i)] (h : ι κ) (f : Π₀ (i : ι), β i) :
                                                    instance DFinsupp.hasAdd₂ {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [(i : ι) → (j : α i) → AddZeroClass (δ i j)] :
                                                    Add (Π₀ (i : ι) (j : α i), δ i j)
                                                    Equations
                                                    • DFinsupp.hasAdd₂ = inferInstance
                                                    instance DFinsupp.addZeroClass₂ {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [(i : ι) → (j : α i) → AddZeroClass (δ i j)] :
                                                    AddZeroClass (Π₀ (i : ι) (j : α i), δ i j)
                                                    Equations
                                                    • DFinsupp.addZeroClass₂ = inferInstance
                                                    instance DFinsupp.addMonoid₂ {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [(i : ι) → (j : α i) → AddMonoid (δ i j)] :
                                                    AddMonoid (Π₀ (i : ι) (j : α i), δ i j)
                                                    Equations
                                                    • DFinsupp.addMonoid₂ = inferInstance
                                                    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.
                                                    Instances For
                                                      @[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)) :
                                                      @[simp]
                                                      theorem DFinsupp.extendWith_zero {ι : Type u} {α : Option ιType v} [DecidableEq ι] [(i : Option ι) → Zero (α i)] (x : α none) :
                                                      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.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        @[simp]
                                                        theorem DFinsupp.equivProdDFinsupp_symm_apply {ι : Type u} {α : Option ιType v} [(i : Option ι) → Zero (α i)] (f : α none × Π₀ (i : ι), α (some i)) :
                                                        DFinsupp.equivProdDFinsupp.symm f = DFinsupp.extendWith f.1 f.2
                                                        @[simp]
                                                        theorem DFinsupp.equivProdDFinsupp_apply {ι : Type u} {α : Option ιType v} [(i : Option ι) → Zero (α i)] (f : Π₀ (i : Option ι), α i) :
                                                        DFinsupp.equivProdDFinsupp f = (f none, DFinsupp.comapDomain some f)
                                                        theorem DFinsupp.equivProdDFinsupp_add {ι : Type u} {α : Option ιType v} [(i : Option ι) → AddZeroClass (α i)] (f g : Π₀ (i : Option ι), α i) :
                                                        DFinsupp.equivProdDFinsupp (f + g) = DFinsupp.equivProdDFinsupp f + DFinsupp.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) :
                                                        DFinsupp.mapRange f hf (g₁ + g₂) = DFinsupp.mapRange f hf g₁ + DFinsupp.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.

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

                                                          DFinsupp.mapRange.addMonoidHom as an AddEquiv.

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