Documentation

Mathlib.Data.Finsupp.Defs

Type of functions with finite support #

For any type α and any type M with zero, we define the type Finsupp α M (notation: α →₀ M) of finitely supported functions from α to M, i.e. the functions which are zero everywhere on α except on a finite set.

Functions with finite support are used (at least) in the following parts of the library:

Some other constructions are naturally equivalent to α →₀ M with some α and M but are defined in a different way in the library:

Most of the theory assumes that the range is a commutative additive monoid. This gives us the big sum operator as a powerful way to construct Finsupp elements, which is defined in Algebra/BigOperators/Finsupp.

-- Porting note: the semireducibility remark no longer applies in Lean 4, afaict. Many constructions based on α →₀ M use semireducible type tags to avoid reusing unwanted type instances. E.g., MonoidAlgebra, AddMonoidAlgebra, and types based on these two have non-pointwise multiplication.

Main declarations #

Notations #

This file adds α →₀ M as a global notation for Finsupp α M.

We also use the following convention for Type* variables in this file

Implementation notes #

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

TODO #

structure Finsupp (α : Type u_13) (M : Type u_14) [Zero M] :
Type (max u_13 u_14)
  • support : Finset α

    The support of a finitely supported function (aka Finsupp).

  • toFun : αM

    The underlying function of a bundled finitely supported function (aka Finsupp).

  • mem_support_toFun : ∀ (a : α), a s.support Finsupp.toFun s a 0

    The witness that the support of a Finsupp is indeed the exact locus where its underlying function is nonzero.

Finsupp α M, denoted α →₀ M, is the type of functions f : α → M such that f x = 0 for all but finitely many x.

Instances For

    Finsupp α M, denoted α →₀ M, is the type of functions f : α → M such that f x = 0 for all but finitely many x.

    Equations
    Instances For

      Basic declarations about Finsupp #

      instance Finsupp.funLike {α : Type u_1} {M : Type u_5} [Zero M] :
      FunLike (α →₀ M) α fun x => M
      Equations
      • Finsupp.funLike = { coe := Finsupp.toFun, coe_injective' := (_ : ∀ ⦃a₁ a₂ : α →₀ M⦄, a₁.toFun = a₂.toFuna₁ = a₂) }
      instance Finsupp.coeFun {α : Type u_1} {M : Type u_5} [Zero M] :
      CoeFun (α →₀ M) fun x => αM

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

      Equations
      • Finsupp.coeFun = inferInstance
      theorem Finsupp.ext {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {g : α →₀ M} (h : ∀ (a : α), f a = g a) :
      f = g
      @[deprecated FunLike.ext_iff]
      theorem Finsupp.ext_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {g : α →₀ M} :
      f = g ∀ (a : α), f a = g a
      @[deprecated FunLike.coe_fn_eq]
      theorem Finsupp.coeFn_inj {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {g : α →₀ M} :
      f = g f = g
      @[deprecated FunLike.coe_injective]
      theorem Finsupp.coeFn_injective {α : Type u_1} {M : Type u_5} [Zero M] :
      Function.Injective FunLike.coe
      @[deprecated FunLike.congr_fun]
      theorem Finsupp.congr_fun {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {g : α →₀ M} (h : f = g) (a : α) :
      f a = g a
      @[simp]
      theorem Finsupp.coe_mk {α : Type u_1} {M : Type u_5} [Zero M] (f : αM) (s : Finset α) (h : ∀ (a : α), a s f a 0) :
      { support := s, toFun := f, mem_support_toFun := h } = f
      instance Finsupp.zero {α : Type u_1} {M : Type u_5} [Zero M] :
      Zero (α →₀ M)
      Equations
      • Finsupp.zero = { zero := { support := , toFun := 0, mem_support_toFun := (_ : ∀ (x : α), x OfNat.ofNat (αM) 0 Zero.toOfNat0 x 0) } }
      @[simp]
      theorem Finsupp.coe_zero {α : Type u_1} {M : Type u_5} [Zero M] :
      0 = 0
      theorem Finsupp.zero_apply {α : Type u_1} {M : Type u_5} [Zero M] {a : α} :
      0 a = 0
      @[simp]
      theorem Finsupp.support_zero {α : Type u_1} {M : Type u_5} [Zero M] :
      0.support =
      instance Finsupp.inhabited {α : Type u_1} {M : Type u_5} [Zero M] :
      Equations
      • Finsupp.inhabited = { default := 0 }
      @[simp]
      theorem Finsupp.mem_support_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} :
      a f.support f a 0
      @[simp]
      theorem Finsupp.fun_support_eq {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) :
      Function.support f = f.support
      theorem Finsupp.not_mem_support_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} :
      ¬a f.support f a = 0
      @[simp]
      theorem Finsupp.coe_eq_zero {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
      f = 0 f = 0
      theorem Finsupp.ext_iff' {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {g : α →₀ M} :
      f = g f.support = g.support ∀ (x : α), x f.supportf x = g x
      @[simp]
      theorem Finsupp.support_eq_empty {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
      f.support = f = 0
      theorem Finsupp.support_nonempty_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
      Finset.Nonempty f.support f 0
      theorem Finsupp.nonzero_iff_exists {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
      f 0 a, f a 0
      theorem Finsupp.card_support_eq_zero {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
      Finset.card f.support = 0 f = 0
      instance Finsupp.decidableEq {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] [DecidableEq M] :
      Equations
      theorem Finsupp.finite_support {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) :
      theorem Finsupp.support_subset_iff {α : Type u_1} {M : Type u_5} [Zero M] {s : Set α} {f : α →₀ M} :
      f.support s ∀ (a : α), ¬a sf a = 0
      @[simp]
      theorem Finsupp.equivFunOnFinite_symm_apply_support {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] (f : αM) :
      (Finsupp.equivFunOnFinite.symm f).support = Set.Finite.toFinset (_ : Set.Finite (Function.support f))
      @[simp]
      theorem Finsupp.equivFunOnFinite_symm_apply_toFun {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] (f : αM) :
      ∀ (a : α), ↑(Finsupp.equivFunOnFinite.symm f) a = f a
      @[simp]
      theorem Finsupp.equivFunOnFinite_apply {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] :
      ∀ (a : α →₀ M) (a_1 : α), Finsupp.equivFunOnFinite a a_1 = a a_1
      def Finsupp.equivFunOnFinite {α : Type u_1} {M : Type u_5} [Zero M] [Finite α] :
      (α →₀ M) (αM)

      Given Finite α, equivFunOnFinite is the Equiv between α →₀ β and α → β. (All functions on a finite type are finitely supported.)

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem Finsupp.equivFunOnFinite_symm_coe {M : Type u_5} [Zero M] {α : Type u_13} [Finite α] (f : α →₀ M) :
        Finsupp.equivFunOnFinite.symm f = f
        @[simp]
        theorem Equiv.finsuppUnique_apply {M : Type u_5} [Zero M] {ι : Type u_13} [Unique ι] :
        ∀ (a : ι →₀ M), Equiv.finsuppUnique a = a default
        @[simp]
        theorem Equiv.finsuppUnique_symm_apply_support_val {M : Type u_5} [Zero M] {ι : Type u_13} [Unique ι] :
        ∀ (a : M), (Equiv.finsuppUnique.symm a).support.val = Multiset.map Subtype.val Finset.univ.val
        @[simp]
        theorem Equiv.finsuppUnique_symm_apply_toFun {M : Type u_5} [Zero M] {ι : Type u_13} [Unique ι] :
        ∀ (a : M) (a_1 : ι), ↑(Equiv.finsuppUnique.symm a) a_1 = (Equiv.funUnique ι M).symm a a_1
        noncomputable def Equiv.finsuppUnique {M : Type u_5} [Zero M] {ι : Type u_13} [Unique ι] :
        (ι →₀ M) M

        If α has a unique term, the type of finitely supported functions α →₀ β is equivalent to β.

        Equations
        Instances For
          theorem Finsupp.unique_ext {α : Type u_1} {M : Type u_5} [Zero M] [Unique α] {f : α →₀ M} {g : α →₀ M} (h : f default = g default) :
          f = g
          theorem Finsupp.unique_ext_iff {α : Type u_1} {M : Type u_5} [Zero M] [Unique α] {f : α →₀ M} {g : α →₀ M} :
          f = g f default = g default

          Declarations about single #

          def Finsupp.single {α : Type u_1} {M : Type u_5} [Zero M] (a : α) (b : M) :
          α →₀ M

          single a b is the finitely supported function with value b at a and zero otherwise.

          Equations
          Instances For
            theorem Finsupp.single_apply {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {a' : α} {b : M} [Decidable (a = a')] :
            ↑(Finsupp.single a b) a' = if a = a' then b else 0
            theorem Finsupp.single_apply_left {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : αβ} (hf : Function.Injective f) (x : α) (z : α) (y : M) :
            ↑(Finsupp.single (f x) y) (f z) = ↑(Finsupp.single x y) z
            theorem Finsupp.single_eq_set_indicator {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} :
            ↑(Finsupp.single a b) = Set.indicator {a} fun x => b
            @[simp]
            theorem Finsupp.single_eq_same {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} :
            ↑(Finsupp.single a b) a = b
            @[simp]
            theorem Finsupp.single_eq_of_ne {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {a' : α} {b : M} (h : a a') :
            ↑(Finsupp.single a b) a' = 0
            theorem Finsupp.single_eq_update {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] (a : α) (b : M) :
            theorem Finsupp.single_eq_pi_single {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] (a : α) (b : M) :
            @[simp]
            theorem Finsupp.single_zero {α : Type u_1} {M : Type u_5} [Zero M] (a : α) :
            theorem Finsupp.single_of_single_apply {α : Type u_1} {M : Type u_5} [Zero M] (a : α) (a' : α) (b : M) :
            theorem Finsupp.support_single_ne_zero {α : Type u_1} {M : Type u_5} [Zero M] {b : M} (a : α) (hb : b 0) :
            (Finsupp.single a b).support = {a}
            theorem Finsupp.support_single_subset {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} :
            (Finsupp.single a b).support {a}
            theorem Finsupp.single_apply_mem {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} (x : α) :
            ↑(Finsupp.single a b) x {0, b}
            theorem Finsupp.range_single_subset {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} :
            Set.range ↑(Finsupp.single a b) {0, b}
            theorem Finsupp.single_injective {α : Type u_1} {M : Type u_5} [Zero M] (a : α) :

            Finsupp.single a b is injective in b. For the statement that it is injective in a, see Finsupp.single_left_injective

            theorem Finsupp.single_apply_eq_zero {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {x : α} {b : M} :
            ↑(Finsupp.single a b) x = 0 x = ab = 0
            theorem Finsupp.single_apply_ne_zero {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {x : α} {b : M} :
            ↑(Finsupp.single a b) x 0 x = a b 0
            theorem Finsupp.mem_support_single {α : Type u_1} {M : Type u_5} [Zero M] (a : α) (a' : α) (b : M) :
            a (Finsupp.single a' b).support a = a' b 0
            theorem Finsupp.eq_single_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} {b : M} :
            f = Finsupp.single a b f.support {a} f a = b
            theorem Finsupp.single_eq_single_iff {α : Type u_1} {M : Type u_5} [Zero M] (a₁ : α) (a₂ : α) (b₁ : M) (b₂ : M) :
            Finsupp.single a₁ b₁ = Finsupp.single a₂ b₂ a₁ = a₂ b₁ = b₂ b₁ = 0 b₂ = 0
            theorem Finsupp.single_left_injective {α : Type u_1} {M : Type u_5} [Zero M] {b : M} (h : b 0) :

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

            theorem Finsupp.single_left_inj {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {a' : α} {b : M} (h : b 0) :
            theorem Finsupp.support_single_ne_bot {α : Type u_1} {M : Type u_5} [Zero M] {b : M} (i : α) (h : b 0) :
            (Finsupp.single i b).support
            theorem Finsupp.support_single_disjoint {α : Type u_1} {M : Type u_5} [Zero M] {b : M} {b' : M} (hb : b 0) (hb' : b' 0) {i : α} {j : α} :
            Disjoint (Finsupp.single i b).support (Finsupp.single j b').support i j
            @[simp]
            theorem Finsupp.single_eq_zero {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} :
            Finsupp.single a b = 0 b = 0
            theorem Finsupp.single_swap {α : Type u_1} {M : Type u_5} [Zero M] (a₁ : α) (a₂ : α) (b : M) :
            ↑(Finsupp.single a₁ b) a₂ = ↑(Finsupp.single a₂ b) a₁
            theorem Finsupp.unique_single {α : Type u_1} {M : Type u_5} [Zero M] [Unique α] (x : α →₀ M) :
            x = Finsupp.single default (x default)
            @[simp]
            theorem Finsupp.unique_single_eq_iff {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {a' : α} {b : M} [Unique α] {b' : M} :
            theorem Finsupp.support_eq_singleton {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} :
            f.support = {a} f a 0 f = Finsupp.single a (f a)
            theorem Finsupp.support_eq_singleton' {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} :
            f.support = {a} b x, f = Finsupp.single a b
            theorem Finsupp.card_support_eq_one {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
            Finset.card f.support = 1 a, f a 0 f = Finsupp.single a (f a)
            theorem Finsupp.card_support_eq_one' {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
            Finset.card f.support = 1 a b x, f = Finsupp.single a b
            theorem Finsupp.support_subset_singleton {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} :
            f.support {a} f = Finsupp.single a (f a)
            theorem Finsupp.support_subset_singleton' {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} :
            f.support {a} b, f = Finsupp.single a b
            theorem Finsupp.card_support_le_one {α : Type u_1} {M : Type u_5} [Zero M] [Nonempty α] {f : α →₀ M} :
            Finset.card f.support 1 a, f = Finsupp.single a (f a)
            theorem Finsupp.card_support_le_one' {α : Type u_1} {M : Type u_5} [Zero M] [Nonempty α] {f : α →₀ M} :
            Finset.card f.support 1 a b, f = Finsupp.single a b
            @[simp]
            theorem Finsupp.equivFunOnFinite_single {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] [Finite α] (x : α) (m : M) :
            Finsupp.equivFunOnFinite (Finsupp.single x m) = Pi.single x m
            @[simp]
            theorem Finsupp.equivFunOnFinite_symm_single {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] [Finite α] (x : α) (m : M) :
            Finsupp.equivFunOnFinite.symm (Pi.single x m) = Finsupp.single x m

            Declarations about update #

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

            Replace the value of a α →₀ M at a given point a : α by a given value b : M. If b = 0, this amounts to removing a from the Finsupp.support. Otherwise, if a was not in the Finsupp.support, it is added to it.

            This is the finitely-supported version of Function.update.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem Finsupp.coe_update {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) [DecidableEq α] :
              ↑(Finsupp.update f a b) = Function.update (f) a b
              @[simp]
              theorem Finsupp.update_self {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) :
              Finsupp.update f a (f a) = f
              @[simp]
              theorem Finsupp.zero_update {α : Type u_1} {M : Type u_5} [Zero M] (a : α) (b : M) :
              theorem Finsupp.support_update {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) [DecidableEq α] [DecidableEq M] :
              (Finsupp.update f a b).support = if b = 0 then Finset.erase f.support a else insert a f.support
              @[simp]
              theorem Finsupp.support_update_zero {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) [DecidableEq α] :
              (Finsupp.update f a 0).support = Finset.erase f.support a
              theorem Finsupp.support_update_ne_zero {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) {b : M} [DecidableEq α] (h : b 0) :
              (Finsupp.update f a b).support = insert a f.support

              Declarations about erase #

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

              erase a f is the finitely supported function equal to f except at a where it is equal to 0. If a is not in the support of f then erase a f = f.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem Finsupp.support_erase {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] {a : α} {f : α →₀ M} :
                (Finsupp.erase a f).support = Finset.erase f.support a
                @[simp]
                theorem Finsupp.erase_same {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {f : α →₀ M} :
                ↑(Finsupp.erase a f) a = 0
                @[simp]
                theorem Finsupp.erase_ne {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {a' : α} {f : α →₀ M} (h : a' a) :
                ↑(Finsupp.erase a f) a' = f a'
                @[simp]
                theorem Finsupp.erase_single {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {b : M} :
                theorem Finsupp.erase_single_ne {α : Type u_1} {M : Type u_5} [Zero M] {a : α} {a' : α} {b : M} (h : a a') :
                @[simp]
                theorem Finsupp.erase_of_not_mem_support {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {a : α} (haf : ¬a f.support) :
                @[simp]
                theorem Finsupp.erase_zero {α : Type u_1} {M : Type u_5} [Zero M] (a : α) :

                Declarations about onFinset #

                def Finsupp.onFinset {α : Type u_1} {M : Type u_5} [Zero M] (s : Finset α) (f : αM) (hf : ∀ (a : α), f a 0a s) :
                α →₀ M

                Finsupp.onFinset s f hf is the finsupp function representing f restricted to the finset s. The function must be 0 outside of s. Use this when the set needs to be filtered anyways, otherwise a better set representation is often available.

                Equations
                Instances For
                  @[simp]
                  theorem Finsupp.onFinset_apply {α : Type u_1} {M : Type u_5} [Zero M] {s : Finset α} {f : αM} {hf : ∀ (a : α), f a 0a s} {a : α} :
                  ↑(Finsupp.onFinset s f hf) a = f a
                  @[simp]
                  theorem Finsupp.support_onFinset_subset {α : Type u_1} {M : Type u_5} [Zero M] {s : Finset α} {f : αM} {hf : ∀ (a : α), f a 0a s} :
                  (Finsupp.onFinset s f hf).support s
                  theorem Finsupp.mem_support_onFinset {α : Type u_1} {M : Type u_5} [Zero M] {s : Finset α} {f : αM} (hf : ∀ (a : α), f a 0a s) {a : α} :
                  a (Finsupp.onFinset s f hf).support f a 0
                  theorem Finsupp.support_onFinset {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq M] {s : Finset α} {f : αM} (hf : ∀ (a : α), f a 0a s) :
                  (Finsupp.onFinset s f hf).support = Finset.filter (fun a => f a 0) s
                  noncomputable def Finsupp.ofSupportFinite {α : Type u_1} {M : Type u_5} [Zero M] (f : αM) (hf : Set.Finite (Function.support f)) :
                  α →₀ M

                  The natural Finsupp induced by the function f given that it has finite support.

                  Equations
                  Instances For
                    theorem Finsupp.ofSupportFinite_coe {α : Type u_1} {M : Type u_5} [Zero M] {f : αM} {hf : Set.Finite (Function.support f)} :
                    instance Finsupp.canLift {α : Type u_1} {M : Type u_5} [Zero M] :
                    CanLift (αM) (α →₀ M) FunLike.coe fun f => Set.Finite (Function.support f)
                    Equations

                    Declarations about mapRange #

                    def Finsupp.mapRange {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : MN) (hf : f 0 = 0) (g : α →₀ M) :
                    α →₀ N

                    The composition of f : M → N and g : α →₀ M is mapRange f hf g : α →₀ N, which is well-defined when f 0 = 0.

                    This preserves the structure on f, and exists in various bundled forms for when f is itself bundled (defined in Data/Finsupp/Basic):

                    • Finsupp.mapRange.equiv
                    • Finsupp.mapRange.zeroHom
                    • Finsupp.mapRange.addMonoidHom
                    • Finsupp.mapRange.addEquiv
                    • Finsupp.mapRange.linearMap
                    • Finsupp.mapRange.linearEquiv
                    Equations
                    Instances For
                      @[simp]
                      theorem Finsupp.mapRange_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {f : MN} {hf : f 0 = 0} {g : α →₀ M} {a : α} :
                      ↑(Finsupp.mapRange f hf g) a = f (g a)
                      @[simp]
                      theorem Finsupp.mapRange_zero {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {f : MN} {hf : f 0 = 0} :
                      @[simp]
                      theorem Finsupp.mapRange_id {α : Type u_1} {M : Type u_5} [Zero M] (g : α →₀ M) :
                      Finsupp.mapRange id (_ : id 0 = id 0) g = g
                      theorem Finsupp.mapRange_comp {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] (f : NP) (hf : f 0 = 0) (f₂ : MN) (hf₂ : f₂ 0 = 0) (h : (f f₂) 0 = 0) (g : α →₀ M) :
                      Finsupp.mapRange (f f₂) h g = Finsupp.mapRange f hf (Finsupp.mapRange f₂ hf₂ g)
                      theorem Finsupp.support_mapRange {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {f : MN} {hf : f 0 = 0} {g : α →₀ M} :
                      (Finsupp.mapRange f hf g).support g.support
                      @[simp]
                      theorem Finsupp.mapRange_single {α : Type u_1} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {f : MN} {hf : f 0 = 0} {a : α} {b : M} :
                      theorem Finsupp.support_mapRange_of_injective {ι : Type u_4} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] {e : MN} (he0 : e 0 = 0) (f : ι →₀ M) (he : Function.Injective e) :
                      (Finsupp.mapRange e he0 f).support = f.support

                      Declarations about embDomain #

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

                      Given f : α ↪ β and v : α →₀ M, Finsupp.embDomain f v : β →₀ M is the finitely supported function whose value at f a : β is v a. For a b : β outside the range of f, it is zero.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem Finsupp.support_embDomain {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) (v : α →₀ M) :
                        (Finsupp.embDomain f v).support = Finset.map f v.support
                        @[simp]
                        theorem Finsupp.embDomain_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) :
                        @[simp]
                        theorem Finsupp.embDomain_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) (v : α →₀ M) (a : α) :
                        ↑(Finsupp.embDomain f v) (f a) = v a
                        theorem Finsupp.embDomain_notin_range {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) (v : α →₀ M) (a : β) (h : ¬a Set.range f) :
                        ↑(Finsupp.embDomain f v) a = 0
                        theorem Finsupp.embDomain_injective {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) :
                        @[simp]
                        theorem Finsupp.embDomain_inj {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : α β} {l₁ : α →₀ M} {l₂ : α →₀ M} :
                        Finsupp.embDomain f l₁ = Finsupp.embDomain f l₂ l₁ = l₂
                        @[simp]
                        theorem Finsupp.embDomain_eq_zero {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] {f : α β} {l : α →₀ M} :
                        theorem Finsupp.embDomain_mapRange {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [Zero M] [Zero N] (f : α β) (g : MN) (p : α →₀ M) (hg : g 0 = 0) :
                        theorem Finsupp.single_of_embDomain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (l : α →₀ M) (f : α β) (a : β) (b : M) (hb : b 0) (h : Finsupp.embDomain f l = Finsupp.single a b) :
                        x, l = Finsupp.single x b f x = a
                        @[simp]
                        theorem Finsupp.embDomain_single {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α β) (a : α) (m : M) :

                        Declarations about zipWith #

                        def Finsupp.zipWith {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] (f : MNP) (hf : f 0 0 = 0) (g₁ : α →₀ M) (g₂ : α →₀ N) :
                        α →₀ P

                        Given finitely supported functions g₁ : α →₀ M and g₂ : α →₀ N and function f : M → N → P, Finsupp.zipWith f hf g₁ g₂ is the finitely supported function α →₀ P satisfying zipWith f hf g₁ g₂ a = f (g₁ a) (g₂ a), which is well-defined when f 0 0 = 0.

                        Equations
                        Instances For
                          @[simp]
                          theorem Finsupp.zipWith_apply {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] {f : MNP} {hf : f 0 0 = 0} {g₁ : α →₀ M} {g₂ : α →₀ N} {a : α} :
                          ↑(Finsupp.zipWith f hf g₁ g₂) a = f (g₁ a) (g₂ a)
                          theorem Finsupp.support_zipWith {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [Zero M] [Zero N] [Zero P] [D : DecidableEq α] {f : MNP} {hf : f 0 0 = 0} {g₁ : α →₀ M} {g₂ : α →₀ N} :
                          (Finsupp.zipWith f hf g₁ g₂).support g₁.support g₂.support

                          Additive monoid structure on α →₀ M #

                          instance Finsupp.add {α : Type u_1} {M : Type u_5} [AddZeroClass M] :
                          Add (α →₀ M)
                          Equations
                          @[simp]
                          theorem Finsupp.coe_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f : α →₀ M) (g : α →₀ M) :
                          ↑(f + g) = f + g
                          theorem Finsupp.add_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (g₁ : α →₀ M) (g₂ : α →₀ M) (a : α) :
                          ↑(g₁ + g₂) a = g₁ a + g₂ a
                          theorem Finsupp.support_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] [DecidableEq α] {g₁ : α →₀ M} {g₂ : α →₀ M} :
                          (g₁ + g₂).support g₁.support g₂.support
                          theorem Finsupp.support_add_eq {α : Type u_1} {M : Type u_5} [AddZeroClass M] [DecidableEq α] {g₁ : α →₀ M} {g₂ : α →₀ M} (h : Disjoint g₁.support g₂.support) :
                          (g₁ + g₂).support = g₁.support g₂.support
                          @[simp]
                          theorem Finsupp.single_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (b₁ : M) (b₂ : M) :
                          Finsupp.single a (b₁ + b₂) = Finsupp.single a b₁ + Finsupp.single a b₂
                          instance Finsupp.addZeroClass {α : Type u_1} {M : Type u_5} [AddZeroClass M] :
                          Equations
                          @[simp]
                          theorem Finsupp.singleAddHom_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (b : M) :
                          def Finsupp.singleAddHom {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) :
                          M →+ α →₀ M

                          Finsupp.single as an AddMonoidHom.

                          See Finsupp.lsingle in LinearAlgebra/Finsupp for the stronger version as a linear map.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem Finsupp.applyAddHom_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (g : α →₀ M) :
                            ↑(Finsupp.applyAddHom a) g = g a
                            def Finsupp.applyAddHom {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) :
                            (α →₀ M) →+ M

                            Evaluation of a function f : α →₀ M at a point as an additive monoid homomorphism.

                            See Finsupp.lapply in LinearAlgebra/Finsupp for the stronger version as a linear map.

                            Equations
                            • Finsupp.applyAddHom a = { toZeroHom := { toFun := fun g => g a, map_zero' := (_ : 0 a = 0) }, map_add' := (_ : ∀ (x x_1 : α →₀ M), ↑(x + x_1) a = x a + x_1 a) }
                            Instances For
                              @[simp]
                              theorem Finsupp.coeFnAddHom_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] :
                              ∀ (a : α →₀ M) (a_1 : α), Finsupp.coeFnAddHom a a_1 = a a_1
                              noncomputable def Finsupp.coeFnAddHom {α : Type u_1} {M : Type u_5} [AddZeroClass M] :
                              (α →₀ M) →+ αM

                              Coercion from a Finsupp to a function type is an AddMonoidHom.

                              Equations
                              • Finsupp.coeFnAddHom = { toZeroHom := { toFun := FunLike.coe, map_zero' := (_ : 0 = 0) }, map_add' := (_ : ∀ (f g : α →₀ M), ↑(f + g) = f + g) }
                              Instances For
                                theorem Finsupp.update_eq_single_add_erase {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f : α →₀ M) (a : α) (b : M) :
                                theorem Finsupp.update_eq_erase_add_single {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f : α →₀ M) (a : α) (b : M) :
                                theorem Finsupp.single_add_erase {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (f : α →₀ M) :
                                Finsupp.single a (f a) + Finsupp.erase a f = f
                                theorem Finsupp.erase_add_single {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (f : α →₀ M) :
                                Finsupp.erase a f + Finsupp.single a (f a) = f
                                @[simp]
                                theorem Finsupp.erase_add {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (f : α →₀ M) (f' : α →₀ M) :
                                @[simp]
                                theorem Finsupp.eraseAddHom_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (f : α →₀ M) :
                                def Finsupp.eraseAddHom {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) :
                                (α →₀ M) →+ α →₀ M

                                Finsupp.erase as an AddMonoidHom.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  theorem Finsupp.induction {α : Type u_1} {M : Type u_5} [AddZeroClass M] {p : (α →₀ M) → Prop} (f : α →₀ M) (h0 : p 0) (ha : (a : α) → (b : M) → (f : α →₀ M) → ¬a f.supportb 0p fp (Finsupp.single a b + f)) :
                                  p f
                                  theorem Finsupp.induction₂ {α : Type u_1} {M : Type u_5} [AddZeroClass M] {p : (α →₀ M) → Prop} (f : α →₀ M) (h0 : p 0) (ha : (a : α) → (b : M) → (f : α →₀ M) → ¬a f.supportb 0p fp (f + Finsupp.single a b)) :
                                  p f
                                  theorem Finsupp.induction_linear {α : Type u_1} {M : Type u_5} [AddZeroClass M] {p : (α →₀ M) → Prop} (f : α →₀ M) (h0 : p 0) (hadd : (f g : α →₀ M) → p fp gp (f + g)) (hsingle : (a : α) → (b : M) → p (Finsupp.single a b)) :
                                  p f
                                  @[simp]
                                  theorem Finsupp.add_closure_setOf_eq_single {α : Type u_1} {M : Type u_5} [AddZeroClass M] :
                                  theorem Finsupp.addHom_ext {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] ⦃f : (α →₀ M) →+ N ⦃g : (α →₀ M) →+ N (H : ∀ (x : α) (y : M), f (Finsupp.single x y) = g (Finsupp.single x y)) :
                                  f = g

                                  If two additive homomorphisms from α →₀ M are equal on each single a b, then they are equal.

                                  theorem Finsupp.addHom_ext' {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] ⦃f : (α →₀ M) →+ N ⦃g : (α →₀ M) →+ N (H : ∀ (x : α), AddMonoidHom.comp f (Finsupp.singleAddHom x) = AddMonoidHom.comp g (Finsupp.singleAddHom x)) :
                                  f = g

                                  If two additive homomorphisms from α →₀ M are equal on each single a b, then they are equal.

                                  We formulate this using equality of AddMonoidHoms so that ext tactic can apply a type-specific extensionality lemma after this one. E.g., if the fiber M is or , then it suffices to verify f (single a 1) = g (single a 1).

                                  theorem Finsupp.mulHom_ext {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddZeroClass M] [MulOneClass N] ⦃f : Multiplicative (α →₀ M) →* N ⦃g : Multiplicative (α →₀ M) →* N (H : ∀ (x : α) (y : M), f (Multiplicative.ofAdd (Finsupp.single x y)) = g (Multiplicative.ofAdd (Finsupp.single x y))) :
                                  f = g
                                  theorem Finsupp.mulHom_ext' {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddZeroClass M] [MulOneClass N] {f : Multiplicative (α →₀ M) →* N} {g : Multiplicative (α →₀ M) →* N} (H : ∀ (x : α), MonoidHom.comp f (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x)) = MonoidHom.comp g (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x))) :
                                  f = g
                                  theorem Finsupp.mapRange_add {α : Type u_1} {M : Type u_5} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] {f : MN} {hf : f 0 = 0} (hf' : ∀ (x y : M), f (x + y) = f x + f y) (v₁ : α →₀ M) (v₂ : α →₀ M) :
                                  Finsupp.mapRange f hf (v₁ + v₂) = Finsupp.mapRange f hf v₁ + Finsupp.mapRange f hf v₂
                                  theorem Finsupp.mapRange_add' {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] [AddMonoidHomClass β M N] {f : β} (v₁ : α →₀ M) (v₂ : α →₀ M) :
                                  Finsupp.mapRange f (_ : f 0 = 0) (v₁ + v₂) = Finsupp.mapRange f (_ : f 0 = 0) v₁ + Finsupp.mapRange f (_ : f 0 = 0) v₂
                                  @[simp]
                                  theorem Finsupp.embDomain.addMonoidHom_apply {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] (f : α β) (v : α →₀ M) :
                                  def Finsupp.embDomain.addMonoidHom {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] (f : α β) :
                                  (α →₀ M) →+ β →₀ M

                                  Bundle Finsupp.embDomain f as an additive map from α →₀ M to β →₀ M.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[simp]
                                    theorem Finsupp.embDomain_add {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] (f : α β) (v : α →₀ M) (w : α →₀ M) :
                                    instance Finsupp.hasNatScalar {α : Type u_1} {M : Type u_5} [AddMonoid M] :
                                    SMul (α →₀ M)

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

                                    Equations
                                    instance Finsupp.addMonoid {α : Type u_1} {M : Type u_5} [AddMonoid M] :
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    instance Finsupp.addCommMonoid {α : Type u_1} {M : Type u_5} [AddCommMonoid M] :
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    instance Finsupp.neg {α : Type u_1} {G : Type u_9} [NegZeroClass G] :
                                    Neg (α →₀ G)
                                    Equations
                                    @[simp]
                                    theorem Finsupp.coe_neg {α : Type u_1} {G : Type u_9} [NegZeroClass G] (g : α →₀ G) :
                                    ↑(-g) = -g
                                    theorem Finsupp.neg_apply {α : Type u_1} {G : Type u_9} [NegZeroClass G] (g : α →₀ G) (a : α) :
                                    ↑(-g) a = -g a
                                    theorem Finsupp.mapRange_neg {α : Type u_1} {G : Type u_9} {H : Type u_10} [NegZeroClass G] [NegZeroClass H] {f : GH} {hf : f 0 = 0} (hf' : ∀ (x : G), f (-x) = -f x) (v : α →₀ G) :
                                    theorem Finsupp.mapRange_neg' {α : Type u_1} {β : Type u_2} {G : Type u_9} {H : Type u_10} [AddGroup G] [SubtractionMonoid H] [AddMonoidHomClass β G H] {f : β} (v : α →₀ G) :
                                    Finsupp.mapRange f (_ : f 0 = 0) (-v) = -Finsupp.mapRange f (_ : f 0 = 0) v
                                    instance Finsupp.sub {α : Type u_1} {G : Type u_9} [SubNegZeroMonoid G] :
                                    Sub (α →₀ G)
                                    Equations
                                    @[simp]
                                    theorem Finsupp.coe_sub {α : Type u_1} {G : Type u_9} [SubNegZeroMonoid G] (g₁ : α →₀ G) (g₂ : α →₀ G) :
                                    ↑(g₁ - g₂) = g₁ - g₂
                                    theorem Finsupp.sub_apply {α : Type u_1} {G : Type u_9} [SubNegZeroMonoid G] (g₁ : α →₀ G) (g₂ : α →₀ G) (a : α) :
                                    ↑(g₁ - g₂) a = g₁ a - g₂ a
                                    theorem Finsupp.mapRange_sub {α : Type u_1} {G : Type u_9} {H : Type u_10} [SubNegZeroMonoid G] [SubNegZeroMonoid H] {f : GH} {hf : f 0 = 0} (hf' : ∀ (x y : G), f (x - y) = f x - f y) (v₁ : α →₀ G) (v₂ : α →₀ G) :
                                    Finsupp.mapRange f hf (v₁ - v₂) = Finsupp.mapRange f hf v₁ - Finsupp.mapRange f hf v₂
                                    theorem Finsupp.mapRange_sub' {α : Type u_1} {β : Type u_2} {G : Type u_9} {H : Type u_10} [AddGroup G] [SubtractionMonoid H] [AddMonoidHomClass β G H] {f : β} (v₁ : α →₀ G) (v₂ : α →₀ G) :
                                    Finsupp.mapRange f (_ : f 0 = 0) (v₁ - v₂) = Finsupp.mapRange f (_ : f 0 = 0) v₁ - Finsupp.mapRange f (_ : f 0 = 0) v₂
                                    instance Finsupp.hasIntScalar {α : Type u_1} {G : Type u_9} [AddGroup G] :
                                    SMul (α →₀ G)

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

                                    Equations
                                    instance Finsupp.addGroup {α : Type u_1} {G : Type u_9} [AddGroup G] :
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    instance Finsupp.addCommGroup {α : Type u_1} {G : Type u_9} [AddCommGroup G] :
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    theorem Finsupp.single_add_single_eq_single_add_single {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {k : α} {l : α} {m : α} {n : α} {u : M} {v : M} (hu : u 0) (hv : v 0) :
                                    Finsupp.single k u + Finsupp.single l v = Finsupp.single m u + Finsupp.single n v k = m l = n u = v k = n l = m u + v = 0 k = l m = n
                                    @[simp]
                                    theorem Finsupp.support_neg {α : Type u_1} {G : Type u_9} [AddGroup G] (f : α →₀ G) :
                                    (-f).support = f.support
                                    theorem Finsupp.support_sub {α : Type u_1} {G : Type u_9} [DecidableEq α] [AddGroup G] {f : α →₀ G} {g : α →₀ G} :
                                    (f - g).support f.support g.support
                                    theorem Finsupp.erase_eq_sub_single {α : Type u_1} {G : Type u_9} [AddGroup G] (f : α →₀ G) (a : α) :
                                    Finsupp.erase a f = f - Finsupp.single a (f a)
                                    theorem Finsupp.update_eq_sub_add_single {α : Type u_1} {G : Type u_9} [AddGroup G] (f : α →₀ G) (a : α) (b : G) :