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)

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

  • 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 self.support self.toFun a 0

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

Instances For
    theorem Finsupp.mem_support_toFun {α : Type u_13} {M : Type u_14} [Zero M] (self : α →₀ M) (a : α) :
    a self.support self.toFun 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.

    Equations
    Instances For

      Basic declarations about Finsupp #

      instance Finsupp.instFunLike {α : Type u_1} {M : Type u_5} [Zero M] :
      FunLike (α →₀ M) α M
      Equations
      • Finsupp.instFunLike = { coe := Finsupp.toFun, coe_injective' := }
      instance Finsupp.instCoeFun {α : Type u_1} {M : Type u_5} [Zero M] :
      CoeFun (α →₀ M) fun (x : α →₀ M) => αM

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

      Equations
      • Finsupp.instCoeFun = 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
      theorem Finsupp.ne_iff {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} {g : α →₀ M} :
      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.instZero {α : Type u_1} {M : Type u_5} [Zero M] :
      Zero (α →₀ M)
      Equations
      • Finsupp.instZero = { zero := { support := , toFun := 0, mem_support_toFun := } }
      @[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] :
      instance Finsupp.instInhabited {α : Type u_1} {M : Type u_5} [Zero M] :
      Equations
      • Finsupp.instInhabited = { 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 : α} :
      af.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 xf.support, f 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} :
      f.support.Nonempty f 0
      theorem Finsupp.card_support_eq_zero {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
      f.support.card = 0 f = 0
      instance Finsupp.instDecidableEq {α : 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) :
      (Function.support f).Finite
      theorem Finsupp.support_subset_iff {α : Type u_1} {M : Type u_5} [Zero M] {s : Set α} {f : α →₀ M} :
      f.support s as, f 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 = .toFinset
      @[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
      • Finsupp.equivFunOnFinite = { toFun := DFunLike.coe, invFun := fun (f : αM) => { support := .toFinset, toFun := f, mem_support_toFun := }, left_inv := , right_inv := }
      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 = a
        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) = {a}.indicator 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₁
            instance Finsupp.instNontrivial {α : Type u_1} {M : Type u_5} [Zero M] [Nonempty α] [Nontrivial M] :
            Equations
            • =
            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.apply_single {α : Type u_1} {N : Type u_7} {P : Type u_8} [AddCommMonoid N] [AddCommMonoid P] {F : Type u_13} [FunLike F N P] [AddMonoidHomClass F N P] (e : F) (a : α) (n : N) (b : α) :
            e ((Finsupp.single a n) b) = (Finsupp.single a (e n)) b
            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 : M), b 0 f = Finsupp.single a b
            theorem Finsupp.card_support_eq_one {α : Type u_1} {M : Type u_5} [Zero M] {f : α →₀ M} :
            f.support.card = 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} :
            f.support.card = 1 ∃ (a : α) (b : M), b 0 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 : M), f = Finsupp.single a b
            theorem Finsupp.card_support_le_one {α : Type u_1} {M : Type u_5} [Zero M] [Nonempty α] {f : α →₀ M} :
            f.support.card 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} :
            f.support.card 1 ∃ (a : α) (b : M), 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
            • f.update a b = { support := if b = 0 then f.support.erase a else insert a f.support, toFun := Function.update (f) a b, mem_support_toFun := }
            Instances For
              @[simp]
              theorem Finsupp.coe_update {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) [DecidableEq α] :
              (f.update a b) = Function.update (f) a b
              @[simp]
              theorem Finsupp.update_self {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) :
              f.update 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] :
              (f.update a b).support = if b = 0 then f.support.erase 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 α] :
              (f.update a 0).support = f.support.erase 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) :
              (f.update a b).support = insert a f.support
              theorem Finsupp.support_update_subset {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) {b : M} [DecidableEq α] [DecidableEq M] :
              (f.update a b).support insert a f.support
              theorem Finsupp.update_comm {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) {a₁ : α} {a₂ : α} (h : a₁ a₂) (m₁ : M) (m₂ : M) :
              (f.update a₁ m₁).update a₂ m₂ = (f.update a₂ m₂).update a₁ m₁
              @[simp]
              theorem Finsupp.update_idem {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) (c : M) :
              (f.update a b).update a c = f.update a c

              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
              • Finsupp.erase a f = { support := f.support.erase a, toFun := fun (a' : α) => if a' = a then 0 else f a', mem_support_toFun := }
              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 = f.support.erase 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'
                theorem Finsupp.erase_apply {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] {a : α} {a' : α} {f : α →₀ M} :
                (Finsupp.erase a f) a' = if a' = a then 0 else 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 : af.support) :
                @[simp]
                theorem Finsupp.erase_zero {α : Type u_1} {M : Type u_5} [Zero M] (a : α) :
                theorem Finsupp.erase_eq_update_zero {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) :
                Finsupp.erase a f = f.update a 0
                theorem Finsupp.erase_update_of_ne {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) {a : α} {a' : α} (ha : a a') (b : M) :
                Finsupp.erase a (f.update a' b) = (Finsupp.erase a f).update a' b
                theorem Finsupp.erase_idem {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) :
                @[simp]
                theorem Finsupp.update_erase_eq_update {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) :
                (Finsupp.erase a f).update a b = f.update a b
                @[simp]
                theorem Finsupp.erase_update_eq_erase {α : Type u_1} {M : Type u_5} [Zero M] (f : α →₀ M) (a : α) (b : M) :
                Finsupp.erase a (f.update a b) = Finsupp.erase a f

                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 : (Function.support f).Finite) :
                  α →₀ 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 : (Function.support f).Finite} :
                    instance Finsupp.instCanLift {α : Type u_1} {M : Type u_5} [Zero M] :
                    CanLift (αM) (α →₀ M) DFunLike.coe fun (f : αM) => (Function.support f).Finite
                    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 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 : aSet.range f) :
                        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
                          @[simp]
                          theorem Finsupp.zipWith_single_single {α : 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) (a : α) (m : M) (n : N) :

                          Additive monoid structure on α →₀ M #

                          instance Finsupp.instAdd {α : 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.instAddZeroClass {α : Type u_1} {M : Type u_5} [AddZeroClass M] :
                          Equations
                          Equations
                          • =
                          noncomputable def Finsupp.addEquivFunOnFinite {M : Type u_5} [AddZeroClass M] {ι : Type u_13} [Finite ι] :
                          (ι →₀ M) ≃+ (ιM)

                          When ι is finite and M is an AddMonoid, then Finsupp.equivFunOnFinite gives an AddEquiv

                          Equations
                          • Finsupp.addEquivFunOnFinite = let __spread.0 := Finsupp.equivFunOnFinite; { toEquiv := __spread.0, map_add' := }
                          Instances For
                            noncomputable def AddEquiv.finsuppUnique {M : Type u_5} [AddZeroClass M] {ι : Type u_13} [Unique ι] :
                            (ι →₀ M) ≃+ M

                            AddEquiv between (ι →₀ M) and M, when ι has a unique element

                            Equations
                            • AddEquiv.finsuppUnique = let __spread.0 := Equiv.finsuppUnique; { toEquiv := __spread.0, map_add' := }
                            Instances For
                              theorem AddEquiv.finsuppUnique_symm {M : Type u_13} [AddZeroClass M] (d : M) :
                              AddEquiv.finsuppUnique.symm d = Finsupp.single () d
                              Equations
                              • =
                              instance Finsupp.instIsCancelAdd {α : Type u_1} {M : Type u_5} [AddZeroClass M] [IsCancelAdd 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
                              Instances For
                                @[simp]
                                theorem Finsupp.applyAddHom_apply {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (g : α →₀ M) :
                                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
                                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 = { toFun := DFunLike.coe, map_zero' := , map_add' := }
                                  Instances For
                                    theorem Finsupp.update_eq_single_add_erase {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f : α →₀ M) (a : α) (b : M) :
                                    f.update a b = Finsupp.single a b + Finsupp.erase a f
                                    theorem Finsupp.update_eq_erase_add_single {α : Type u_1} {M : Type u_5} [AddZeroClass M] (f : α →₀ M) (a : α) (b : M) :
                                    f.update a b = Finsupp.erase a f + Finsupp.single a b
                                    theorem Finsupp.single_add_erase {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (f : α →₀ M) :
                                    theorem Finsupp.erase_add_single {α : Type u_1} {M : Type u_5} [AddZeroClass M] (a : α) (f : α →₀ M) :
                                    @[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
                                    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), af.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), af.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] :
                                      AddSubmonoid.closure {f : α →₀ M | ∃ (a : α) (b : M), f = Finsupp.single a b} =
                                      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 : α), f.comp (Finsupp.singleAddHom x) = g.comp (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 : α), f.comp (AddMonoidHom.toMultiplicative (Finsupp.singleAddHom x)) = g.comp (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] [FunLike β M N] [AddMonoidHomClass β M N] {f : β} (v₁ : α →₀ M) (v₂ : α →₀ M) :
                                      Finsupp.mapRange f (v₁ + v₂) = Finsupp.mapRange f v₁ + Finsupp.mapRange f 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
                                      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.instNatSMul {α : 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.instAddMonoid {α : Type u_1} {M : Type u_5} [AddMonoid M] :
                                        Equations
                                        instance Finsupp.instAddCommMonoid {α : Type u_1} {M : Type u_5} [AddCommMonoid M] :
                                        Equations
                                        instance Finsupp.instNeg {α : 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] [FunLike β G H] [AddMonoidHomClass β G H] {f : β} (v : α →₀ G) :
                                        Finsupp.mapRange f (-v) = -Finsupp.mapRange f v
                                        instance Finsupp.instSub {α : 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] [FunLike β G H] [AddMonoidHomClass β G H] {f : β} (v₁ : α →₀ G) (v₂ : α →₀ G) :
                                        Finsupp.mapRange f (v₁ - v₂) = Finsupp.mapRange f v₁ - Finsupp.mapRange f v₂
                                        instance Finsupp.instIntSMul {α : 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.instAddGroup {α : Type u_1} {G : Type u_9} [AddGroup G] :
                                        Equations
                                        instance Finsupp.instAddCommGroup {α : Type u_1} {G : Type u_9} [AddCommGroup G] :
                                        Equations
                                        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 : α) :
                                        theorem Finsupp.update_eq_sub_add_single {α : Type u_1} {G : Type u_9} [AddGroup G] (f : α →₀ G) (a : α) (b : G) :
                                        f.update a b = f - Finsupp.single a (f a) + Finsupp.single a b