Documentation

Mathlib.Data.Finsupp.Basic

Miscellaneous definitions, lemmas, and constructions using finsupp #

Main declarations #

Implementation notes #

This file is a noncomputable theory and uses classical logic throughout.

TODO #

Declarations about graph #

def Finsupp.graph {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) :
Finset (α × M)

The graph of a finitely supported function over its support, i.e. the finset of input and output pairs with non-zero outputs.

Equations
  • f.graph = Finset.map { toFun := fun (a : α) => (a, f a), inj' := } f.support
Instances For
    theorem Finsupp.mk_mem_graph_iff {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {m : M} {f : α →₀ M} :
    (a, m) f.graph f a = m m 0
    @[simp]
    theorem Finsupp.mem_graph_iff {α : Type u_1} {M : Type u_5} [Zero M] {c : α × M} {f : α →₀ M} :
    c f.graph f c.1 = c.2 c.2 0
    theorem Finsupp.mk_mem_graph {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) {a : α} (ha : a f.support) :
    (a, f a) f.graph
    theorem Finsupp.apply_eq_of_mem_graph {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {m : M} {f : α →₀ M} (h : (a, m) f.graph) :
    f a = m
    @[simp]
    theorem Finsupp.not_mem_graph_snd_zero {α : Type u_1} {M : Type u_5} [Zero M] (a : α) (f : α →₀ M) :
    (a, 0)f.graph
    @[simp]
    theorem Finsupp.image_fst_graph {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] (f : α →₀ M) :
    Finset.image Prod.fst f.graph = f.support
    theorem Finsupp.graph_injective (α : Type u_13) (M : Type u_14) [Zero M] :
    Function.Injective Finsupp.graph
    @[simp]
    theorem Finsupp.graph_inj {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {g : α →₀ M} :
    f.graph = g.graph f = g
    @[simp]
    theorem Finsupp.graph_zero {α : Type u_1} {M : Type u_5} [Zero M] :
    @[simp]
    theorem Finsupp.graph_eq_empty {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
    f.graph = f = 0

    Declarations about mapRange #

    @[simp]
    theorem Finsupp.mapRange.equiv_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : M N) (hf : f 0 = 0) (hf' : f.symm 0 = 0) (g : α →₀ M) :
    (Finsupp.mapRange.equiv f hf hf') g = Finsupp.mapRange (f) hf g
    def Finsupp.mapRange.equiv {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : M N) (hf : f 0 = 0) (hf' : f.symm 0 = 0) :
    (α →₀ M) (α →₀ N)

    Finsupp.mapRange as an equiv.

    Equations
    Instances For
      @[simp]
      theorem Finsupp.mapRange.equiv_refl {α : Type u_1} {M : Type u_5} [Zero M] :
      theorem Finsupp.mapRange.equiv_trans {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] (f : M N) (hf : f 0 = 0) (hf' : f.symm 0 = 0) (f₂ : N P) (hf₂ : f₂ 0 = 0) (hf₂' : f₂.symm 0 = 0) :
      Finsupp.mapRange.equiv (f.trans f₂) = (Finsupp.mapRange.equiv f hf hf').trans (Finsupp.mapRange.equiv f₂ hf₂ hf₂')
      @[simp]
      theorem Finsupp.mapRange.equiv_symm {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : M N) (hf : f 0 = 0) (hf' : f.symm 0 = 0) :
      (Finsupp.mapRange.equiv f hf hf').symm = Finsupp.mapRange.equiv f.symm hf' hf
      @[simp]
      theorem Finsupp.mapRange.zeroHom_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : ZeroHom M N) (g : α →₀ M) :
      def Finsupp.mapRange.zeroHom {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : ZeroHom M N) :
      ZeroHom (α →₀ M) (α →₀ N)

      Composition with a fixed zero-preserving homomorphism is itself a zero-preserving homomorphism on functions.

      Equations
      Instances For
        theorem Finsupp.mapRange.zeroHom_comp {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] (f : ZeroHom N P) (f₂ : ZeroHom M N) :
        @[simp]
        theorem Finsupp.mapRange.addMonoidHom_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] (f : M →+ N) (g : α →₀ M) :
        def Finsupp.mapRange.addMonoidHom {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] (f : M →+ N) :
        (α →₀ M) →+ α →₀ N

        Composition with a fixed additive homomorphism is itself an additive homomorphism on functions.

        Equations
        Instances For
          theorem Finsupp.mapRange.addMonoidHom_comp {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] (f : N →+ P) (f₂ : M →+ N) :
          theorem Finsupp.mapRange_multiset_sum {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] {F : Type u_13} [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (m : Multiset (α →₀ M)) :
          Finsupp.mapRange f m.sum = (Multiset.map (fun (x : α →₀ M) => Finsupp.mapRange f x) m).sum
          theorem Finsupp.mapRange_finset_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] {F : Type u_13} [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (s : Finset ι) (g : ια →₀ M) :
          Finsupp.mapRange f (xs, g x) = xs, Finsupp.mapRange f (g x)
          @[simp]
          theorem Finsupp.mapRange.addEquiv_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] (f : M ≃+ N) (g : α →₀ M) :
          def Finsupp.mapRange.addEquiv {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] (f : M ≃+ N) :
          (α →₀ M) ≃+ (α →₀ N)

          Finsupp.mapRange.AddMonoidHom as an equiv.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem Finsupp.mapRange.addEquiv_trans {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] (f : M ≃+ N) (f₂ : N ≃+ P) :
            @[simp]
            theorem Finsupp.mapRange.addEquiv_symm {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] (f : M ≃+ N) :
            @[simp]
            @[simp]
            theorem Finsupp.mapRange.addEquiv_toEquiv {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] (f : M ≃+ N) :

            Declarations about equivCongrLeft #

            def Finsupp.equivMapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) (l : α →₀ M) :
            β →₀ M

            Given f : α ≃ β, we can map l : α →₀ M to equivMapDomain f l : β →₀ M (computably) by mapping the support forwards and the function backwards.

            Equations
            Instances For
              @[simp]
              theorem Finsupp.equivMapDomain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) (l : α →₀ M) (b : β) :
              (Finsupp.equivMapDomain f l) b = l (f.symm b)
              theorem Finsupp.equivMapDomain_symm_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) (l : β →₀ M) (a : α) :
              (Finsupp.equivMapDomain f.symm l) a = l (f a)
              @[simp]
              theorem Finsupp.equivMapDomain_refl {α : Type u_1} {M : Type u_5} [Zero M] (l : α →₀ M) :
              theorem Finsupp.equivMapDomain_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [Zero M] (f : α β) (g : β γ) (l : α →₀ M) :
              theorem Finsupp.equivMapDomain_trans' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [Zero M] (f : α β) (g : β γ) :
              @[simp]
              theorem Finsupp.equivMapDomain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) (a : α) (b : M) :
              @[simp]
              theorem Finsupp.equivMapDomain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : α β} :
              @[simp]
              theorem Finsupp.sum_equivMapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [Zero M] [AddCommMonoid N] (f : α β) (l : α →₀ M) (g : βMN) :
              (Finsupp.equivMapDomain f l).sum g = l.sum fun (a : α) (m : M) => g (f a) m
              @[simp]
              theorem Finsupp.prod_equivMapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [Zero M] [CommMonoid N] (f : α β) (l : α →₀ M) (g : βMN) :
              (Finsupp.equivMapDomain f l).prod g = l.prod fun (a : α) (m : M) => g (f a) m
              def Finsupp.equivCongrLeft {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) :
              (α →₀ M) (β →₀ M)

              Given f : α ≃ β, the finitely supported function spaces are also in bijection: (α →₀ M) ≃ (β →₀ M).

              This is the finitely-supported version of Equiv.piCongrLeft.

              Equations
              Instances For
                @[simp]
                theorem Finsupp.equivCongrLeft_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) (l : α →₀ M) :
                @[simp]
                theorem Finsupp.equivCongrLeft_symm {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) :
                @[simp]
                theorem Nat.cast_finsupp_prod {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [CommSemiring R] (g : αM) :
                (f.prod g) = f.prod fun (a : α) (b : M) => (g a b)
                @[simp]
                theorem Nat.cast_finsupp_sum {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [CommSemiring R] (g : αM) :
                (f.sum g) = f.sum fun (a : α) (b : M) => (g a b)
                @[simp]
                theorem Int.cast_finsupp_prod {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [CommRing R] (g : αM) :
                (f.prod g) = f.prod fun (a : α) (b : M) => (g a b)
                @[simp]
                theorem Int.cast_finsupp_sum {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [CommRing R] (g : αM) :
                (f.sum g) = f.sum fun (a : α) (b : M) => (g a b)
                @[simp]
                theorem Rat.cast_finsupp_sum {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [DivisionRing R] [CharZero R] (g : αM) :
                (f.sum g) = f.sum fun (a : α) (b : M) => (g a b)
                @[simp]
                theorem Rat.cast_finsupp_prod {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] (f : α →₀ M) [Field R] [CharZero R] (g : αM) :
                (f.prod g) = f.prod fun (a : α) (b : M) => (g a b)

                Declarations about mapDomain #

                def Finsupp.mapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (f : αβ) (v : α →₀ M) :
                β →₀ M

                Given f : α → β and v : α →₀ M, mapDomain f v : β →₀ M is the finitely supported function whose value at a : β is the sum of v x over all x such that f x = a.

                Equations
                Instances For
                  theorem Finsupp.mapDomain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {f : αβ} (hf : Function.Injective f) (x : α →₀ M) (a : α) :
                  (Finsupp.mapDomain f x) (f a) = x a
                  theorem Finsupp.mapDomain_notin_range {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {f : αβ} (x : α →₀ M) (a : β) (h : aSet.range f) :
                  @[simp]
                  theorem Finsupp.mapDomain_id {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {v : α →₀ M} :
                  theorem Finsupp.mapDomain_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [AddCommMonoid M] {v : α →₀ M} {f : αβ} {g : βγ} :
                  @[simp]
                  theorem Finsupp.mapDomain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {f : αβ} {a : α} {b : M} :
                  @[simp]
                  theorem Finsupp.mapDomain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {f : αβ} :
                  theorem Finsupp.mapDomain_congr {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {v : α →₀ M} {f : αβ} {g : αβ} (h : xv.support, f x = g x) :
                  theorem Finsupp.mapDomain_add {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {v₁ : α →₀ M} {v₂ : α →₀ M} {f : αβ} :
                  @[simp]
                  theorem Finsupp.mapDomain_equiv_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {f : α β} (x : α →₀ M) (a : β) :
                  (Finsupp.mapDomain (f) x) a = x (f.symm a)
                  @[simp]
                  theorem Finsupp.mapDomain.addMonoidHom_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (f : αβ) (v : α →₀ M) :
                  def Finsupp.mapDomain.addMonoidHom {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (f : αβ) :
                  (α →₀ M) →+ β →₀ M

                  Finsupp.mapDomain is an AddMonoidHom.

                  Equations
                  Instances For
                    theorem Finsupp.mapDomain.addMonoidHom_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [AddCommMonoid M] (f : βγ) (g : αβ) :
                    theorem Finsupp.mapDomain_finset_sum {α : Type u_1} {β : Type u_2} {ι : Type u_4} {M : Type u_5} [AddCommMonoid M] {f : αβ} {s : Finset ι} {v : ια →₀ M} :
                    Finsupp.mapDomain f (is, v i) = is, Finsupp.mapDomain f (v i)
                    theorem Finsupp.mapDomain_sum {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [Zero N] {f : αβ} {s : α →₀ N} {v : αNα →₀ M} :
                    Finsupp.mapDomain f (s.sum v) = s.sum fun (a : α) (b : N) => Finsupp.mapDomain f (v a b)
                    theorem Finsupp.mapDomain_support {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] [DecidableEq β] {f : αβ} {s : α →₀ M} :
                    (Finsupp.mapDomain f s).support Finset.image f s.support
                    theorem Finsupp.mapDomain_apply' {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (S : Set α) {f : αβ} (x : α →₀ M) (hS : x.support S) (hf : Set.InjOn f S) {a : α} (ha : a S) :
                    (Finsupp.mapDomain f x) (f a) = x a
                    theorem Finsupp.mapDomain_support_of_injOn {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] [DecidableEq β] {f : αβ} (s : α →₀ M) (hf : Set.InjOn f s.support) :
                    (Finsupp.mapDomain f s).support = Finset.image f s.support
                    theorem Finsupp.mapDomain_support_of_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] [DecidableEq β] {f : αβ} (hf : Function.Injective f) (s : α →₀ M) :
                    (Finsupp.mapDomain f s).support = Finset.image f s.support
                    theorem Finsupp.sum_mapDomain_index {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] {f : αβ} {s : α →₀ M} {h : βMN} (h_zero : ∀ (b : β), h b 0 = 0) (h_add : ∀ (b : β) (m₁ m₂ : M), h b (m₁ + m₂) = h b m₁ + h b m₂) :
                    (Finsupp.mapDomain f s).sum h = s.sum fun (a : α) (m : M) => h (f a) m
                    theorem Finsupp.prod_mapDomain_index {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [CommMonoid N] {f : αβ} {s : α →₀ M} {h : βMN} (h_zero : ∀ (b : β), h b 0 = 1) (h_add : ∀ (b : β) (m₁ m₂ : M), h b (m₁ + m₂) = h b m₁ * h b m₂) :
                    (Finsupp.mapDomain f s).prod h = s.prod fun (a : α) (m : M) => h (f a) m
                    @[simp]
                    theorem Finsupp.sum_mapDomain_index_addMonoidHom {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] {f : αβ} {s : α →₀ M} (h : βM →+ N) :
                    ((Finsupp.mapDomain f s).sum fun (b : β) (m : M) => (h b) m) = s.sum fun (a : α) (m : M) => (h (f a)) m

                    A version of sum_mapDomain_index that takes a bundled AddMonoidHom, rather than separate linearity hypotheses.

                    theorem Finsupp.embDomain_eq_mapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (f : α β) (v : α →₀ M) :
                    theorem Finsupp.sum_mapDomain_index_inj {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] {f : αβ} {s : α →₀ M} {h : βMN} (hf : Function.Injective f) :
                    (Finsupp.mapDomain f s).sum h = s.sum fun (a : α) (b : M) => h (f a) b
                    theorem Finsupp.prod_mapDomain_index_inj {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [CommMonoid N] {f : αβ} {s : α →₀ M} {h : βMN} (hf : Function.Injective f) :
                    (Finsupp.mapDomain f s).prod h = s.prod fun (a : α) (b : M) => h (f a) b
                    theorem Finsupp.mapDomain_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] {f : αβ} (hf : Function.Injective f) :
                    @[simp]
                    theorem Finsupp.mapDomainEmbedding_apply {α : Type u_13} {β : Type u_14} (f : α β) (v : α →₀ ) :
                    def Finsupp.mapDomainEmbedding {α : Type u_13} {β : Type u_14} (f : α β) :

                    When f is an embedding we have an embedding (α →₀ ℕ) ↪ (β →₀ ℕ) given by mapDomain.

                    Equations
                    Instances For
                      theorem Finsupp.mapDomain_mapRange {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] (f : αβ) (v : α →₀ M) (g : MN) (h0 : g 0 = 0) (hadd : ∀ (x y : M), g (x + y) = g x + g y) :

                      When g preserves addition, mapRange and mapDomain commute.

                      theorem Finsupp.sum_update_add {α : Type u_1} {β : Type u_2} {ι : Type u_4} [AddCommMonoid α] [AddCommMonoid β] (f : ι →₀ α) (i : ι) (a : α) (g : ιαβ) (hg : ∀ (i : ι), g i 0 = 0) (hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂) :
                      (f.update i a).sum g + g i (f i) = f.sum g + g i a
                      theorem Finsupp.mapDomain_injOn {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (S : Set α) {f : αβ} (hf : Set.InjOn f S) :
                      Set.InjOn (Finsupp.mapDomain f) {w : α →₀ M | w.support S}
                      theorem Finsupp.equivMapDomain_eq_mapDomain {α : Type u_1} {β : Type u_2} {M : Type u_13} [AddCommMonoid M] (f : α β) (l : α →₀ M) :

                      Declarations about comapDomain #

                      @[simp]
                      theorem Finsupp.comapDomain_support {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : αβ) (l : β →₀ M) (hf : Set.InjOn f (f ⁻¹' l.support)) :
                      (Finsupp.comapDomain f l hf).support = l.support.preimage f hf
                      def Finsupp.comapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : αβ) (l : β →₀ M) (hf : Set.InjOn f (f ⁻¹' l.support)) :
                      α →₀ M

                      Given f : α → β, l : β →₀ M and a proof hf that f is injective on the preimage of l.support, comapDomain f l hf is the finitely supported function from α to M given by composing l with f.

                      Equations
                      • Finsupp.comapDomain f l hf = { support := l.support.preimage f hf, toFun := fun (a : α) => l (f a), mem_support_toFun := }
                      Instances For
                        @[simp]
                        theorem Finsupp.comapDomain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : αβ) (l : β →₀ M) (hf : Set.InjOn f (f ⁻¹' l.support)) (a : α) :
                        (Finsupp.comapDomain f l hf) a = l (f a)
                        theorem Finsupp.sum_comapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [Zero M] [AddCommMonoid N] (f : αβ) (l : β →₀ M) (g : βMN) (hf : Set.BijOn f (f ⁻¹' l.support) l.support) :
                        (Finsupp.comapDomain f l ).sum (g f) = l.sum g
                        theorem Finsupp.eq_zero_of_comapDomain_eq_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (f : αβ) (l : β →₀ M) (hf : Set.BijOn f (f ⁻¹' l.support) l.support) :
                        Finsupp.comapDomain f l = 0l = 0
                        theorem Finsupp.embDomain_comapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : α β} {g : β →₀ M} (hg : g.support Set.range f) :
                        @[simp]
                        theorem Finsupp.comapDomain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : αβ) (hif : optParam (Set.InjOn f (f ⁻¹' (Finsupp.support 0))) ) :

                        Note the hif argument is needed for this to work in rw.

                        @[simp]
                        theorem Finsupp.comapDomain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : αβ) (a : α) (m : M) (hif : Set.InjOn f (f ⁻¹' (Finsupp.single (f a) m).support)) :
                        theorem Finsupp.comapDomain_add {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] {f : αβ} (v₁ : β →₀ M) (v₂ : β →₀ M) (hv₁ : Set.InjOn f (f ⁻¹' v₁.support)) (hv₂ : Set.InjOn f (f ⁻¹' v₂.support)) (hv₁₂ : Set.InjOn f (f ⁻¹' (v₁ + v₂).support)) :
                        Finsupp.comapDomain f (v₁ + v₂) hv₁₂ = Finsupp.comapDomain f v₁ hv₁ + Finsupp.comapDomain f v₂ hv₂
                        theorem Finsupp.comapDomain_add_of_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] {f : αβ} (hf : Function.Injective f) (v₁ : β →₀ M) (v₂ : β →₀ M) :
                        Finsupp.comapDomain f (v₁ + v₂) = Finsupp.comapDomain f v₁ + Finsupp.comapDomain f v₂

                        A version of Finsupp.comapDomain_add that's easier to use.

                        @[simp]
                        theorem Finsupp.comapDomain.addMonoidHom_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] {f : αβ} (hf : Function.Injective f) (x : β →₀ M) :
                        def Finsupp.comapDomain.addMonoidHom {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] {f : αβ} (hf : Function.Injective f) :
                        (β →₀ M) →+ α →₀ M

                        Finsupp.comapDomain is an AddMonoidHom.

                        Equations
                        Instances For
                          theorem Finsupp.mapDomain_comapDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (f : αβ) (hf : Function.Injective f) (l : β →₀ M) (hl : l.support Set.range f) :

                          Declarations about finitely supported functions whose support is an Option type #

                          def Finsupp.some {α : Type u_1} {M : Type u_5} [Zero M] (f : Option α →₀ M) :
                          α →₀ M

                          Restrict a finitely supported function on Option α to a finitely supported function on α.

                          Equations
                          Instances For
                            @[simp]
                            theorem Finsupp.some_apply {α : Type u_1} {M : Type u_5} [Zero M] (f : Option α →₀ M) (a : α) :
                            f.some a = f (some a)
                            @[simp]
                            theorem Finsupp.some_zero {α : Type u_1} {M : Type u_5} [Zero M] :
                            @[simp]
                            theorem Finsupp.some_add {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (f : Option α →₀ M) (g : Option α →₀ M) :
                            (f + g).some = f.some + g.some
                            @[simp]
                            theorem Finsupp.some_single_none {α : Type u_1} {M : Type u_5} [Zero M] (m : M) :
                            (Finsupp.single none m).some = 0
                            @[simp]
                            theorem Finsupp.some_single_some {α : Type u_1} {M : Type u_5} [Zero M] (a : α) (m : M) :
                            theorem Finsupp.sum_option_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] (f : Option α →₀ M) (b : Option αMN) (h_zero : ∀ (o : Option α), b o 0 = 0) (h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ + b o m₂) :
                            f.sum b = b none (f none) + f.some.sum fun (a : α) => b (some a)
                            theorem Finsupp.prod_option_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [CommMonoid N] (f : Option α →₀ M) (b : Option αMN) (h_zero : ∀ (o : Option α), b o 0 = 1) (h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂) :
                            f.prod b = b none (f none) * f.some.prod fun (a : α) => b (some a)
                            theorem Finsupp.sum_option_index_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} [Semiring R] [AddCommMonoid M] [Module R M] (f : Option α →₀ R) (b : Option αM) :
                            (f.sum fun (o : Option α) (r : R) => r b o) = f none b none + f.some.sum fun (a : α) (r : R) => r b (some a)

                            Declarations about Finsupp.filter #

                            def Finsupp.filter {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [DecidablePred p] (f : α →₀ M) :
                            α →₀ M

                            Finsupp.filter p f is the finitely supported function that is f a if p a is true and 0 otherwise.

                            Equations
                            Instances For
                              theorem Finsupp.filter_apply {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [DecidablePred p] (f : α →₀ M) (a : α) :
                              (Finsupp.filter p f) a = if p a then f a else 0
                              theorem Finsupp.filter_eq_indicator {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [DecidablePred p] (f : α →₀ M) :
                              (Finsupp.filter p f) = {x : α | p x}.indicator f
                              theorem Finsupp.filter_eq_zero_iff {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [DecidablePred p] (f : α →₀ M) :
                              Finsupp.filter p f = 0 ∀ (x : α), p xf x = 0
                              theorem Finsupp.filter_eq_self_iff {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [DecidablePred p] (f : α →₀ M) :
                              Finsupp.filter p f = f ∀ (x : α), f x 0p x
                              @[simp]
                              theorem Finsupp.filter_apply_pos {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [DecidablePred p] (f : α →₀ M) {a : α} (h : p a) :
                              (Finsupp.filter p f) a = f a
                              @[simp]
                              theorem Finsupp.filter_apply_neg {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [DecidablePred p] (f : α →₀ M) {a : α} (h : ¬p a) :
                              (Finsupp.filter p f) a = 0
                              @[simp]
                              theorem Finsupp.support_filter {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [DecidablePred p] (f : α →₀ M) :
                              (Finsupp.filter p f).support = Finset.filter p f.support
                              theorem Finsupp.filter_zero {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [DecidablePred p] :
                              @[simp]
                              theorem Finsupp.filter_single_of_pos {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [DecidablePred p] {a : α} {b : M} (h : p a) :
                              @[simp]
                              theorem Finsupp.filter_single_of_neg {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) [DecidablePred p] {a : α} {b : M} (h : ¬p a) :
                              theorem Finsupp.sum_filter_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] (p : αProp) [DecidablePred p] (f : α →₀ M) [AddCommMonoid N] (g : αMN) :
                              (Finsupp.filter p f).sum g = x(Finsupp.filter p f).support, g x (f x)
                              theorem Finsupp.prod_filter_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] (p : αProp) [DecidablePred p] (f : α →₀ M) [CommMonoid N] (g : αMN) :
                              (Finsupp.filter p f).prod g = x(Finsupp.filter p f).support, g x (f x)
                              @[simp]
                              theorem Finsupp.sum_filter_add_sum_filter_not {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] (p : αProp) [DecidablePred p] (f : α →₀ M) [AddCommMonoid N] (g : αMN) :
                              (Finsupp.filter p f).sum g + (Finsupp.filter (fun (a : α) => ¬p a) f).sum g = f.sum g
                              @[simp]
                              theorem Finsupp.prod_filter_mul_prod_filter_not {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] (p : αProp) [DecidablePred p] (f : α →₀ M) [CommMonoid N] (g : αMN) :
                              (Finsupp.filter p f).prod g * (Finsupp.filter (fun (a : α) => ¬p a) f).prod g = f.prod g
                              @[simp]
                              theorem Finsupp.sum_sub_sum_filter {α : Type u_1} {M : Type u_5} {G : Type u_9} [Zero M] (p : αProp) [DecidablePred p] (f : α →₀ M) [AddCommGroup G] (g : αMG) :
                              f.sum g - (Finsupp.filter p f).sum g = (Finsupp.filter (fun (a : α) => ¬p a) f).sum g
                              @[simp]
                              theorem Finsupp.prod_div_prod_filter {α : Type u_1} {M : Type u_5} {G : Type u_9} [Zero M] (p : αProp) [DecidablePred p] (f : α →₀ M) [CommGroup G] (g : αMG) :
                              f.prod g / (Finsupp.filter p f).prod g = (Finsupp.filter (fun (a : α) => ¬p a) f).prod g
                              theorem Finsupp.filter_pos_add_filter_neg {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f : α →₀ M) (p : αProp) [DecidablePred p] :
                              Finsupp.filter p f + Finsupp.filter (fun (a : α) => ¬p a) f = f

                              Declarations about frange #

                              def Finsupp.frange {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) :

                              frange f is the image of f on the support of f.

                              Equations
                              Instances For
                                theorem Finsupp.mem_frange {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {y : M} :
                                y f.frange y 0 ∃ (x : α), f x = y
                                theorem Finsupp.zero_not_mem_frange {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
                                0f.frange
                                theorem Finsupp.frange_single {α : Type u_1} {M : Type u_5} [Zero M] {x : α} {y : M} :
                                (Finsupp.single x y).frange {y}

                                Declarations about Finsupp.subtypeDomain #

                                def Finsupp.subtypeDomain {α : Type u_1} {M : Type u_5} [Zero M] (p : αProp) (f : α →₀ M) :

                                subtypeDomain p f is the restriction of the finitely supported function f to subtype p.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem Finsupp.support_subtypeDomain {α : Type u_1} {M : Type u_5} [Zero M] {p : αProp} [D : DecidablePred p] {f : α →₀ M} :
                                  (Finsupp.subtypeDomain p f).support = Finset.subtype p f.support
                                  @[simp]
                                  theorem Finsupp.subtypeDomain_apply {α : Type u_1} {M : Type u_5} [Zero M] {p : αProp} {a : Subtype p} {v : α →₀ M} :
                                  (Finsupp.subtypeDomain p v) a = v a
                                  @[simp]
                                  theorem Finsupp.subtypeDomain_zero {α : Type u_1} {M : Type u_5} [Zero M] {p : αProp} :
                                  theorem Finsupp.subtypeDomain_eq_zero_iff' {α : Type u_1} {M : Type u_5} [Zero M] {p : αProp} {f : α →₀ M} :
                                  Finsupp.subtypeDomain p f = 0 ∀ (x : α), p xf x = 0
                                  theorem Finsupp.subtypeDomain_eq_zero_iff {α : Type u_1} {M : Type u_5} [Zero M] {p : αProp} {f : α →₀ M} (hf : xf.support, p x) :
                                  theorem Finsupp.sum_subtypeDomain_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] {p : αProp} [AddCommMonoid N] {v : α →₀ M} {h : αMN} (hp : xv.support, p x) :
                                  ((Finsupp.subtypeDomain p v).sum fun (a : Subtype p) (b : M) => h (a) b) = v.sum h
                                  theorem Finsupp.prod_subtypeDomain_index {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] {p : αProp} [CommMonoid N] {v : α →₀ M} {h : αMN} (hp : xv.support, p x) :
                                  ((Finsupp.subtypeDomain p v).prod fun (a : Subtype p) (b : M) => h (a) b) = v.prod h
                                  @[simp]
                                  theorem Finsupp.subtypeDomain_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] {p : αProp} {v : α →₀ M} {v' : α →₀ M} :
                                  def Finsupp.subtypeDomainAddMonoidHom {α : Type u_1} {M : Type u_5} [AddZeroClass M] {p : αProp} :

                                  subtypeDomain but as an AddMonoidHom.

                                  Equations
                                  Instances For
                                    def Finsupp.filterAddHom {α : Type u_1} {M : Type u_5} [AddZeroClass M] (p : αProp) [DecidablePred p] :
                                    (α →₀ M) →+ α →₀ M

                                    Finsupp.filter as an AddMonoidHom.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem Finsupp.filter_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] {p : αProp} [DecidablePred p] {v : α →₀ M} {v' : α →₀ M} :
                                      theorem Finsupp.subtypeDomain_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} [AddCommMonoid M] {p : αProp} {s : Finset ι} {h : ια →₀ M} :
                                      Finsupp.subtypeDomain p (cs, h c) = cs, Finsupp.subtypeDomain p (h c)
                                      theorem Finsupp.subtypeDomain_finsupp_sum {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] {p : αProp} [Zero N] {s : β →₀ N} {h : βNα →₀ M} :
                                      Finsupp.subtypeDomain p (s.sum h) = s.sum fun (c : β) (d : N) => Finsupp.subtypeDomain p (h c d)
                                      theorem Finsupp.filter_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} [AddCommMonoid M] {p : αProp} [DecidablePred p] (s : Finset ι) (f : ια →₀ M) :
                                      Finsupp.filter p (as, f a) = as, Finsupp.filter p (f a)
                                      theorem Finsupp.filter_eq_sum {α : Type u_1} {M : Type u_5} [AddCommMonoid M] (p : αProp) [DecidablePred p] (f : α →₀ M) :
                                      Finsupp.filter p f = iFinset.filter p f.support, Finsupp.single i (f i)
                                      @[simp]
                                      theorem Finsupp.subtypeDomain_neg {α : Type u_1} {G : Type u_9} [AddGroup G] {p : αProp} {v : α →₀ G} :
                                      @[simp]
                                      theorem Finsupp.subtypeDomain_sub {α : Type u_1} {G : Type u_9} [AddGroup G] {p : αProp} {v : α →₀ G} {v' : α →₀ G} :
                                      @[simp]
                                      theorem Finsupp.single_neg {α : Type u_1} {G : Type u_9} [AddGroup G] (a : α) (b : G) :
                                      @[simp]
                                      theorem Finsupp.single_sub {α : Type u_1} {G : Type u_9} [AddGroup G] (a : α) (b₁ : G) (b₂ : G) :
                                      Finsupp.single a (b₁ - b₂) = Finsupp.single a b₁ - Finsupp.single a b₂
                                      @[simp]
                                      theorem Finsupp.erase_neg {α : Type u_1} {G : Type u_9} [AddGroup G] (a : α) (f : α →₀ G) :
                                      @[simp]
                                      theorem Finsupp.erase_sub {α : Type u_1} {G : Type u_9} [AddGroup G] (a : α) (f₁ : α →₀ G) (f₂ : α →₀ G) :
                                      Finsupp.erase a (f₁ - f₂) = Finsupp.erase a f₁ - Finsupp.erase a f₂
                                      @[simp]
                                      theorem Finsupp.filter_neg {α : Type u_1} {G : Type u_9} [AddGroup G] (p : αProp) [DecidablePred p] (f : α →₀ G) :
                                      @[simp]
                                      theorem Finsupp.filter_sub {α : Type u_1} {G : Type u_9} [AddGroup G] (p : αProp) [DecidablePred p] (f₁ : α →₀ G) (f₂ : α →₀ G) :
                                      Finsupp.filter p (f₁ - f₂) = Finsupp.filter p f₁ - Finsupp.filter p f₂
                                      theorem Finsupp.mem_support_multiset_sum {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {s : Multiset (α →₀ M)} (a : α) :
                                      a s.sum.supportfs, a f.support
                                      theorem Finsupp.mem_support_finset_sum {α : Type u_1} {ι : Type u_4} {M : Type u_5} [AddCommMonoid M] {s : Finset ι} {h : ια →₀ M} (a : α) (ha : a (cs, h c).support) :
                                      cs, a (h c).support

                                      Declarations about curry and uncurry #

                                      def Finsupp.curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (f : α × β →₀ M) :
                                      α →₀ β →₀ M

                                      Given a finitely supported function f from a product type α × β to γ, curry f is the "curried" finitely supported function from α to the type of finitely supported functions from β to γ.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem Finsupp.curry_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (f : α × β →₀ M) (x : α) (y : β) :
                                        (f.curry x) y = f (x, y)
                                        theorem Finsupp.sum_curry_index {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] (f : α × β →₀ M) (g : αβMN) (hg₀ : ∀ (a : α) (b : β), g a b 0 = 0) (hg₁ : ∀ (a : α) (b : β) (c₀ c₁ : M), g a b (c₀ + c₁) = g a b c₀ + g a b c₁) :
                                        (f.curry.sum fun (a : α) (f : β →₀ M) => f.sum (g a)) = f.sum fun (p : α × β) (c : M) => g p.1 p.2 c
                                        def Finsupp.uncurry {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (f : α →₀ β →₀ M) :
                                        α × β →₀ M

                                        Given a finitely supported function f from α to the type of finitely supported functions from β to M, uncurry f is the "uncurried" finitely supported function from α × β to M.

                                        Equations
                                        • f.uncurry = f.sum fun (a : α) (g : β →₀ M) => g.sum fun (b : β) (c : M) => Finsupp.single (a, b) c
                                        Instances For
                                          def Finsupp.finsuppProdEquiv {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] :
                                          (α × β →₀ M) (α →₀ β →₀ M)

                                          finsuppProdEquiv defines the Equiv between ((α × β) →₀ M) and (α →₀ (β →₀ M)) given by currying and uncurrying.

                                          Equations
                                          • Finsupp.finsuppProdEquiv = { toFun := Finsupp.curry, invFun := Finsupp.uncurry, left_inv := , right_inv := }
                                          Instances For
                                            theorem Finsupp.filter_curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (f : α × β →₀ M) (p : αProp) [DecidablePred p] :
                                            (Finsupp.filter (fun (a : α × β) => p a.1) f).curry = Finsupp.filter p f.curry
                                            theorem Finsupp.support_curry {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] [DecidableEq α] (f : α × β →₀ M) :
                                            f.curry.support Finset.image Prod.fst f.support

                                            Declarations about finitely supported functions whose support is a Sum type #

                                            def Finsupp.sumElim {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α →₀ γ) (g : β →₀ γ) :
                                            α β →₀ γ

                                            Finsupp.sumElim f g maps inl x to f x and inr y to g y.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem Finsupp.coe_sumElim {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α →₀ γ) (g : β →₀ γ) :
                                              (f.sumElim g) = Sum.elim f g
                                              theorem Finsupp.sumElim_apply {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α →₀ γ) (g : β →₀ γ) (x : α β) :
                                              (f.sumElim g) x = Sum.elim (f) (g) x
                                              theorem Finsupp.sumElim_inl {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α →₀ γ) (g : β →₀ γ) (x : α) :
                                              (f.sumElim g) (Sum.inl x) = f x
                                              theorem Finsupp.sumElim_inr {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α →₀ γ) (g : β →₀ γ) (x : β) :
                                              (f.sumElim g) (Sum.inr x) = g x
                                              @[simp]
                                              theorem Finsupp.sumFinsuppEquivProdFinsupp_symm_apply {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (fg : (α →₀ γ) × (β →₀ γ)) :
                                              Finsupp.sumFinsuppEquivProdFinsupp.symm fg = fg.1.sumElim fg.2
                                              @[simp]
                                              theorem Finsupp.sumFinsuppEquivProdFinsupp_apply {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α β →₀ γ) :
                                              Finsupp.sumFinsuppEquivProdFinsupp f = (Finsupp.comapDomain Sum.inl f , Finsupp.comapDomain Sum.inr f )
                                              def Finsupp.sumFinsuppEquivProdFinsupp {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] :
                                              (α β →₀ γ) (α →₀ γ) × (β →₀ γ)

                                              The equivalence between (α ⊕ β) →₀ γ and (α →₀ γ) × (β →₀ γ).

                                              This is the Finsupp version of Equiv.sum_arrow_equiv_prod_arrow.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                theorem Finsupp.fst_sumFinsuppEquivProdFinsupp {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α β →₀ γ) (x : α) :
                                                (Finsupp.sumFinsuppEquivProdFinsupp f).1 x = f (Sum.inl x)
                                                theorem Finsupp.snd_sumFinsuppEquivProdFinsupp {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (f : α β →₀ γ) (y : β) :
                                                (Finsupp.sumFinsuppEquivProdFinsupp f).2 y = f (Sum.inr y)
                                                theorem Finsupp.sumFinsuppEquivProdFinsupp_symm_inl {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (fg : (α →₀ γ) × (β →₀ γ)) (x : α) :
                                                (Finsupp.sumFinsuppEquivProdFinsupp.symm fg) (Sum.inl x) = fg.1 x
                                                theorem Finsupp.sumFinsuppEquivProdFinsupp_symm_inr {α : Type u_13} {β : Type u_14} {γ : Type u_15} [Zero γ] (fg : (α →₀ γ) × (β →₀ γ)) (y : β) :
                                                (Finsupp.sumFinsuppEquivProdFinsupp.symm fg) (Sum.inr y) = fg.2 y
                                                @[simp]
                                                theorem Finsupp.sumFinsuppAddEquivProdFinsupp_apply {M : Type u_5} [AddMonoid M] {α : Type u_13} {β : Type u_14} (f : α β →₀ M) :
                                                Finsupp.sumFinsuppAddEquivProdFinsupp f = (Finsupp.comapDomain Sum.inl f , Finsupp.comapDomain Sum.inr f )
                                                @[simp]
                                                theorem Finsupp.sumFinsuppAddEquivProdFinsupp_symm_apply {M : Type u_5} [AddMonoid M] {α : Type u_13} {β : Type u_14} (fg : (α →₀ M) × (β →₀ M)) :
                                                Finsupp.sumFinsuppAddEquivProdFinsupp.symm fg = fg.1.sumElim fg.2
                                                def Finsupp.sumFinsuppAddEquivProdFinsupp {M : Type u_5} [AddMonoid M] {α : Type u_13} {β : Type u_14} :
                                                (α β →₀ M) ≃+ (α →₀ M) × (β →₀ M)

                                                The additive equivalence between (α ⊕ β) →₀ M and (α →₀ M) × (β →₀ M).

                                                This is the Finsupp version of Equiv.sum_arrow_equiv_prod_arrow.

                                                Equations
                                                • Finsupp.sumFinsuppAddEquivProdFinsupp = let __src := Finsupp.sumFinsuppEquivProdFinsupp; { toEquiv := __src, map_add' := }
                                                Instances For
                                                  theorem Finsupp.fst_sumFinsuppAddEquivProdFinsupp {M : Type u_5} [AddMonoid M] {α : Type u_13} {β : Type u_14} (f : α β →₀ M) (x : α) :
                                                  (Finsupp.sumFinsuppAddEquivProdFinsupp f).1 x = f (Sum.inl x)
                                                  theorem Finsupp.snd_sumFinsuppAddEquivProdFinsupp {M : Type u_5} [AddMonoid M] {α : Type u_13} {β : Type u_14} (f : α β →₀ M) (y : β) :
                                                  (Finsupp.sumFinsuppAddEquivProdFinsupp f).2 y = f (Sum.inr y)
                                                  theorem Finsupp.sumFinsuppAddEquivProdFinsupp_symm_inl {M : Type u_5} [AddMonoid M] {α : Type u_13} {β : Type u_14} (fg : (α →₀ M) × (β →₀ M)) (x : α) :
                                                  (Finsupp.sumFinsuppAddEquivProdFinsupp.symm fg) (Sum.inl x) = fg.1 x
                                                  theorem Finsupp.sumFinsuppAddEquivProdFinsupp_symm_inr {M : Type u_5} [AddMonoid M] {α : Type u_13} {β : Type u_14} (fg : (α →₀ M) × (β →₀ M)) (y : β) :
                                                  (Finsupp.sumFinsuppAddEquivProdFinsupp.symm fg) (Sum.inr y) = fg.2 y

                                                  Declarations about scalar multiplication #

                                                  @[simp]
                                                  theorem Finsupp.single_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] [MonoidWithZero R] [MulActionWithZero R M] (a : α) (b : α) (f : αM) (r : R) :
                                                  (Finsupp.single a r) b f a = (Finsupp.single a (r f b)) b
                                                  def Finsupp.comapSMul {α : Type u_1} {M : Type u_5} {G : Type u_9} [Monoid G] [MulAction G α] [AddCommMonoid M] :
                                                  SMul G (α →₀ M)

                                                  Scalar multiplication acting on the domain.

                                                  This is not an instance as it would conflict with the action on the range. See the instance_diamonds test for examples of such conflicts.

                                                  Equations
                                                  Instances For
                                                    theorem Finsupp.comapSMul_def {α : Type u_1} {M : Type u_5} {G : Type u_9} [Monoid G] [MulAction G α] [AddCommMonoid M] (g : G) (f : α →₀ M) :
                                                    g f = Finsupp.mapDomain (fun (x : α) => g x) f
                                                    @[simp]
                                                    theorem Finsupp.comapSMul_single {α : Type u_1} {M : Type u_5} {G : Type u_9} [Monoid G] [MulAction G α] [AddCommMonoid M] (g : G) (a : α) (b : M) :
                                                    def Finsupp.comapMulAction {α : Type u_1} {M : Type u_5} {G : Type u_9} [Monoid G] [MulAction G α] [AddCommMonoid M] :
                                                    MulAction G (α →₀ M)

                                                    Finsupp.comapSMul is multiplicative

                                                    Equations
                                                    Instances For
                                                      def Finsupp.comapDistribMulAction {α : Type u_1} {M : Type u_5} {G : Type u_9} [Monoid G] [MulAction G α] [AddCommMonoid M] :

                                                      Finsupp.comapSMul is distributive

                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        theorem Finsupp.comapSMul_apply {α : Type u_1} {M : Type u_5} {G : Type u_9} [Group G] [MulAction G α] [AddCommMonoid M] (g : G) (f : α →₀ M) (a : α) :
                                                        (g f) a = f (g⁻¹ a)

                                                        When G is a group, Finsupp.comapSMul acts by precomposition with the action of g⁻¹.

                                                        instance Finsupp.smulZeroClass {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] [SMulZeroClass R M] :
                                                        Equations

                                                        Throughout this section, some Monoid and Semiring arguments are specified with {} instead of []. See note [implicit instance arguments].

                                                        @[simp]
                                                        theorem Finsupp.coe_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] [SMulZeroClass R M] (b : R) (v : α →₀ M) :
                                                        (b v) = b v
                                                        theorem Finsupp.smul_apply {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] [SMulZeroClass R M] (b : R) (v : α →₀ M) (a : α) :
                                                        (b v) a = b v a
                                                        theorem IsSMulRegular.finsupp {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] [SMulZeroClass R M] {k : R} (hk : IsSMulRegular M k) :
                                                        instance Finsupp.faithfulSMul {α : Type u_1} {M : Type u_5} {R : Type u_11} [Nonempty α] [Zero M] [SMulZeroClass R M] [FaithfulSMul R M] :
                                                        Equations
                                                        • =
                                                        instance Finsupp.instSMulWithZero {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero R] [Zero M] [SMulWithZero R M] :
                                                        Equations
                                                        instance Finsupp.distribSMul (α : Type u_1) (M : Type u_5) {R : Type u_11} [AddZeroClass M] [DistribSMul R M] :
                                                        Equations
                                                        instance Finsupp.distribMulAction (α : Type u_1) (M : Type u_5) {R : Type u_11} [Monoid R] [AddMonoid M] [DistribMulAction R M] :
                                                        Equations
                                                        instance Finsupp.isScalarTower (α : Type u_1) (M : Type u_5) {R : Type u_11} {S : Type u_12} [Zero M] [SMulZeroClass R M] [SMulZeroClass S M] [SMul R S] [IsScalarTower R S M] :
                                                        Equations
                                                        • =
                                                        instance Finsupp.smulCommClass (α : Type u_1) (M : Type u_5) {R : Type u_11} {S : Type u_12} [Zero M] [SMulZeroClass R M] [SMulZeroClass S M] [SMulCommClass R S M] :
                                                        Equations
                                                        • =
                                                        instance Finsupp.isCentralScalar (α : Type u_1) (M : Type u_5) {R : Type u_11} [Zero M] [SMulZeroClass R M] [SMulZeroClass Rᵐᵒᵖ M] [IsCentralScalar R M] :
                                                        Equations
                                                        • =
                                                        instance Finsupp.module (α : Type u_1) (M : Type u_5) {R : Type u_11} [Semiring R] [AddCommMonoid M] [Module R M] :
                                                        Module R (α →₀ M)
                                                        Equations
                                                        theorem Finsupp.support_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} [AddMonoid M] [SMulZeroClass R M] {b : R} {g : α →₀ M} :
                                                        (b g).support g.support
                                                        @[simp]
                                                        theorem Finsupp.support_smul_eq {α : Type u_1} {M : Type u_5} {R : Type u_11} [Semiring R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M] {b : R} (hb : b 0) {g : α →₀ M} :
                                                        (b g).support = g.support
                                                        @[simp]
                                                        theorem Finsupp.filter_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} {p : αProp} [DecidablePred p] :
                                                        ∀ {x : Monoid R} [inst : AddMonoid M] [inst_1 : DistribMulAction R M] {b : R} {v : α →₀ M}, Finsupp.filter p (b v) = b Finsupp.filter p v
                                                        theorem Finsupp.mapDomain_smul {α : Type u_1} {β : Type u_2} {M : Type u_5} {R : Type u_11} :
                                                        ∀ {x : Monoid R} [inst : AddCommMonoid M] [inst_1 : DistribMulAction R M] {f : αβ} (b : R) (v : α →₀ M), Finsupp.mapDomain f (b v) = b Finsupp.mapDomain f v
                                                        @[simp]
                                                        theorem Finsupp.smul_single {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] [SMulZeroClass R M] (c : R) (a : α) (b : M) :
                                                        theorem Finsupp.smul_single' {α : Type u_1} {R : Type u_11} :
                                                        ∀ {x : Semiring R} (c : R) (a : α) (b : R), c Finsupp.single a b = Finsupp.single a (c * b)
                                                        theorem Finsupp.mapRange_smul {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} :
                                                        ∀ {x : Monoid R} [inst : AddMonoid M] [inst_1 : DistribMulAction R M] [inst_2 : AddMonoid N] [inst_3 : DistribMulAction R N] {f : MN} {hf : f 0 = 0} (c : R) (v : α →₀ M), (∀ (x_1 : M), f (c x_1) = c f x_1)Finsupp.mapRange f hf (c v) = c Finsupp.mapRange f hf v
                                                        theorem Finsupp.smul_single_one {α : Type u_1} {R : Type u_11} [Semiring R] (a : α) (b : R) :
                                                        theorem Finsupp.comapDomain_smul {α : Type u_1} {β : Type u_2} {M : Type u_5} {R : Type u_11} [AddMonoid M] [Monoid R] [DistribMulAction R M] {f : αβ} (r : R) (v : β →₀ M) (hfv : Set.InjOn f (f ⁻¹' v.support)) (hfrv : optParam (Set.InjOn f (f ⁻¹' (r v).support)) ) :
                                                        theorem Finsupp.comapDomain_smul_of_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} {R : Type u_11} [AddMonoid M] [Monoid R] [DistribMulAction R M] {f : αβ} (hf : Function.Injective f) (r : R) (v : β →₀ M) :

                                                        A version of Finsupp.comapDomain_smul that's easier to use.

                                                        theorem Finsupp.sum_smul_index {α : Type u_1} {M : Type u_5} {R : Type u_11} [Semiring R] [AddCommMonoid M] {g : α →₀ R} {b : R} {h : αRM} (h0 : ∀ (i : α), h i 0 = 0) :
                                                        (b g).sum h = g.sum fun (i : α) (a : R) => h i (b * a)
                                                        theorem Finsupp.sum_smul_index' {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} [AddMonoid M] [DistribSMul R M] [AddCommMonoid N] {g : α →₀ M} {b : R} {h : αMN} (h0 : ∀ (i : α), h i 0 = 0) :
                                                        (b g).sum h = g.sum fun (i : α) (c : M) => h i (b c)
                                                        theorem Finsupp.sum_smul_index_addMonoidHom {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} [AddMonoid M] [AddCommMonoid N] [DistribSMul R M] {g : α →₀ M} {b : R} {h : αM →+ N} :
                                                        ((b g).sum fun (a : α) => (h a)) = g.sum fun (i : α) (c : M) => (h i) (b c)

                                                        A version of Finsupp.sum_smul_index' for bundled additive maps.

                                                        instance Finsupp.noZeroSMulDivisors {M : Type u_5} {R : Type u_11} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_13} [NoZeroSMulDivisors R M] :
                                                        Equations
                                                        • =
                                                        def Finsupp.DistribMulActionHom.single {α : Type u_1} {M : Type u_5} {R : Type u_11} [Semiring R] [AddCommMonoid M] [DistribMulAction R M] (a : α) :
                                                        M →+[R] α →₀ M

                                                        Finsupp.single as a DistribMulActionSemiHom.

                                                        See also Finsupp.lsingle for the version as a linear map.

                                                        Equations
                                                        Instances For
                                                          theorem Finsupp.distribMulActionHom_ext {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [DistribMulAction R M] [DistribMulAction R N] {f : (α →₀ M) →+[R] N} {g : (α →₀ M) →+[R] N} (h : ∀ (a : α) (m : M), f (Finsupp.single a m) = g (Finsupp.single a m)) :
                                                          f = g
                                                          theorem Finsupp.distribMulActionHom_ext' {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [DistribMulAction R M] [DistribMulAction R N] {f : (α →₀ M) →+[R] N} {g : (α →₀ M) →+[R] N} (h : ∀ (a : α), f.comp (Finsupp.DistribMulActionHom.single a) = g.comp (Finsupp.DistribMulActionHom.single a)) :
                                                          f = g

                                                          See note [partially-applied ext lemmas].

                                                          instance Finsupp.uniqueOfRight {α : Type u_1} {R : Type u_11} [Zero R] [Subsingleton R] :
                                                          Unique (α →₀ R)

                                                          The Finsupp version of Pi.unique.

                                                          Equations
                                                          • Finsupp.uniqueOfRight = .unique
                                                          instance Finsupp.uniqueOfLeft {α : Type u_1} {R : Type u_11} [Zero R] [IsEmpty α] :
                                                          Unique (α →₀ R)

                                                          The Finsupp version of Pi.uniqueOfIsEmpty.

                                                          Equations
                                                          • Finsupp.uniqueOfLeft = .unique
                                                          @[simp]
                                                          theorem Finsupp.piecewise_support {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [DecidablePred P] (f : Subtype P →₀ M) (g : { a : α // ¬P a } →₀ M) :
                                                          (f.piecewise g).support = (Finset.map (Function.Embedding.subtype P) f.support).disjUnion (Finset.map (Function.Embedding.subtype fun (a : α) => ¬P a) g.support)
                                                          @[simp]
                                                          theorem Finsupp.piecewise_toFun {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [DecidablePred P] (f : Subtype P →₀ M) (g : { a : α // ¬P a } →₀ M) (a : α) :
                                                          (f.piecewise g) a = if h : P a then f a, h else g a, h
                                                          def Finsupp.piecewise {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [DecidablePred P] (f : Subtype P →₀ M) (g : { a : α // ¬P a } →₀ M) :
                                                          α →₀ M

                                                          Combine finitely supported functions over {a // P a} and {a // ¬P a}, by case-splitting on P a.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            @[simp]
                                                            theorem Finsupp.subtypeDomain_piecewise {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [DecidablePred P] (f : Subtype P →₀ M) (g : { a : α // ¬P a } →₀ M) :
                                                            Finsupp.subtypeDomain P (f.piecewise g) = f
                                                            @[simp]
                                                            theorem Finsupp.subtypeDomain_not_piecewise {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [DecidablePred P] (f : Subtype P →₀ M) (g : { a : α // ¬P a } →₀ M) :
                                                            Finsupp.subtypeDomain (fun (x : α) => ¬P x) (f.piecewise g) = g
                                                            @[simp]
                                                            theorem Finsupp.extendDomain_toFun {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [DecidablePred P] (f : Subtype P →₀ M) (a : α) :
                                                            f.extendDomain a = if h : P a then f a, h else 0
                                                            @[simp]
                                                            theorem Finsupp.extendDomain_support {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [DecidablePred P] (f : Subtype P →₀ M) :
                                                            f.extendDomain.support = Finset.map (Function.Embedding.subtype P) f.support
                                                            def Finsupp.extendDomain {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [DecidablePred P] (f : Subtype P →₀ M) :
                                                            α →₀ M

                                                            Extend the domain of a Finsupp by using 0 where P x does not hold.

                                                            Equations
                                                            • f.extendDomain = f.piecewise 0
                                                            Instances For
                                                              theorem Finsupp.extendDomain_eq_embDomain_subtype {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [DecidablePred P] (f : Subtype P →₀ M) :
                                                              theorem Finsupp.support_extendDomain_subset {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [DecidablePred P] (f : Subtype P →₀ M) :
                                                              f.extendDomain.support {x : α | P x}
                                                              @[simp]
                                                              theorem Finsupp.subtypeDomain_extendDomain {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [DecidablePred P] (f : Subtype P →₀ M) :
                                                              Finsupp.subtypeDomain P f.extendDomain = f
                                                              theorem Finsupp.extendDomain_subtypeDomain {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [DecidablePred P] (f : α →₀ M) (hf : af.support, P a) :
                                                              (Finsupp.subtypeDomain P f).extendDomain = f
                                                              @[simp]
                                                              theorem Finsupp.extendDomain_single {α : Type u_1} {M : Type u_13} [Zero M] {P : αProp} [DecidablePred P] (a : Subtype P) (m : M) :
                                                              (Finsupp.single a m).extendDomain = Finsupp.single (a) m
                                                              def Finsupp.restrictSupportEquiv {α : Type u_1} (s : Set α) (M : Type u_13) [AddCommMonoid M] :
                                                              { f : α →₀ M // f.support s } (s →₀ M)

                                                              Given an AddCommMonoid M and s : Set α, restrictSupportEquiv s M is the Equiv between the subtype of finitely supported functions with support contained in s and the type of finitely supported functions from s.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                @[simp]
                                                                theorem Finsupp.domCongr_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (e : α β) (l : α →₀ M) :
                                                                def Finsupp.domCongr {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (e : α β) :
                                                                (α →₀ M) ≃+ (β →₀ M)

                                                                Given AddCommMonoid M and e : α ≃ β, domCongr e is the corresponding Equiv between α →₀ M and β →₀ M.

                                                                This is Finsupp.equivCongrLeft as an AddEquiv.

                                                                Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem Finsupp.domCongr_symm {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddCommMonoid M] (e : α β) :
                                                                  @[simp]
                                                                  theorem Finsupp.domCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [AddCommMonoid M] (e : α β) (f : β γ) :

                                                                  Declarations about sigma types #

                                                                  def Finsupp.split {ι : Type u_4} {M : Type u_5} {αs : ιType u_13} [Zero M] (l : (i : ι) × αs i →₀ M) (i : ι) :
                                                                  αs i →₀ M

                                                                  Given l, a finitely supported function from the sigma type Σ (i : ι), αs i to M and an index element i : ι, split l i is the ith component of l, a finitely supported function from as i to M.

                                                                  This is the Finsupp version of Sigma.curry.

                                                                  Equations
                                                                  Instances For
                                                                    theorem Finsupp.split_apply {ι : Type u_4} {M : Type u_5} {αs : ιType u_13} [Zero M] (l : (i : ι) × αs i →₀ M) (i : ι) (x : αs i) :
                                                                    (l.split i) x = l i, x
                                                                    def Finsupp.splitSupport {ι : Type u_4} {M : Type u_5} {αs : ιType u_13} [Zero M] (l : (i : ι) × αs i →₀ M) :

                                                                    Given l, a finitely supported function from the sigma type Σ (i : ι), αs i to β, split_support l is the finset of indices in ι that appear in the support of l.

                                                                    Equations
                                                                    Instances For
                                                                      theorem Finsupp.mem_splitSupport_iff_nonzero {ι : Type u_4} {M : Type u_5} {αs : ιType u_13} [Zero M] (l : (i : ι) × αs i →₀ M) (i : ι) :
                                                                      i l.splitSupport l.split i 0
                                                                      def Finsupp.splitComp {ι : Type u_4} {M : Type u_5} {N : Type u_7} {αs : ιType u_13} [Zero M] (l : (i : ι) × αs i →₀ M) [Zero N] (g : (i : ι) → (αs i →₀ M)N) (hg : ∀ (i : ι) (x : αs i →₀ M), x = 0 g i x = 0) :
                                                                      ι →₀ N

                                                                      Given l, a finitely supported function from the sigma type Σ i, αs i to β and an ι-indexed family g of functions from (αs i →₀ β) to γ, split_comp defines a finitely supported function from the index type ι to γ given by composing g i with split l i.

                                                                      Equations
                                                                      • l.splitComp g hg = { support := l.splitSupport, toFun := fun (i : ι) => g i (l.split i), mem_support_toFun := }
                                                                      Instances For
                                                                        theorem Finsupp.sigma_support {ι : Type u_4} {M : Type u_5} {αs : ιType u_13} [Zero M] (l : (i : ι) × αs i →₀ M) :
                                                                        l.support = l.splitSupport.sigma fun (i : ι) => (l.split i).support
                                                                        theorem Finsupp.sigma_sum {ι : Type u_4} {M : Type u_5} {N : Type u_7} {αs : ιType u_13} [Zero M] (l : (i : ι) × αs i →₀ M) [AddCommMonoid N] (f : (i : ι) × αs iMN) :
                                                                        l.sum f = il.splitSupport, (l.split i).sum fun (a : αs i) (b : M) => f i, a b
                                                                        noncomputable def Finsupp.sigmaFinsuppEquivPiFinsupp {α : Type u_1} {η : Type u_14} [Fintype η] {ιs : ηType u_15} [Zero α] :
                                                                        ((j : η) × ιs j →₀ α) ((j : η) → ιs j →₀ α)

                                                                        On a Fintype η, Finsupp.split is an equivalence between (Σ (j : η), ιs j) →₀ α and Π j, (ιs j →₀ α).

                                                                        This is the Finsupp version of Equiv.Pi_curry.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem Finsupp.sigmaFinsuppEquivPiFinsupp_apply {α : Type u_1} {η : Type u_14} [Fintype η] {ιs : ηType u_15} [Zero α] (f : (j : η) × ιs j →₀ α) (j : η) (i : ιs j) :
                                                                          (Finsupp.sigmaFinsuppEquivPiFinsupp f j) i = f j, i
                                                                          noncomputable def Finsupp.sigmaFinsuppAddEquivPiFinsupp {η : Type u_14} [Fintype η] {α : Type u_16} {ιs : ηType u_17} [AddMonoid α] :
                                                                          ((j : η) × ιs j →₀ α) ≃+ ((j : η) → ιs j →₀ α)

                                                                          On a Fintype η, Finsupp.split is an additive equivalence between (Σ (j : η), ιs j) →₀ α and Π j, (ιs j →₀ α).

                                                                          This is the AddEquiv version of Finsupp.sigmaFinsuppEquivPiFinsupp.

                                                                          Equations
                                                                          • Finsupp.sigmaFinsuppAddEquivPiFinsupp = let __src := Finsupp.sigmaFinsuppEquivPiFinsupp; { toEquiv := __src, map_add' := }
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem Finsupp.sigmaFinsuppAddEquivPiFinsupp_apply {η : Type u_14} [Fintype η] {α : Type u_16} {ιs : ηType u_17} [AddMonoid α] (f : (j : η) × ιs j →₀ α) (j : η) (i : ιs j) :
                                                                            (Finsupp.sigmaFinsuppAddEquivPiFinsupp f j) i = f j, i