Documentation

Mathlib.Algebra.Group.Finsupp

Additive monoid structure on ι →₀ M #

instance Finsupp.instAdd {ι : Type u_1} {M : Type u_3} [AddZeroClass M] :
Add (ι →₀ M)
Equations
    @[simp]
    theorem Finsupp.coe_add {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (f g : ι →₀ M) :
    ⇑(f + g) = f + g
    theorem Finsupp.add_apply {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (g₁ g₂ : ι →₀ M) (a : ι) :
    (g₁ + g₂) a = g₁ a + g₂ a
    theorem Finsupp.support_add {ι : Type u_1} {M : Type u_3} [AddZeroClass M] {g₁ g₂ : ι →₀ M} [DecidableEq ι] :
    (g₁ + g₂).support g₁.support g₂.support
    theorem Finsupp.support_add_eq {ι : Type u_1} {M : Type u_3} [AddZeroClass M] {g₁ g₂ : ι →₀ M} [DecidableEq ι] (h : Disjoint g₁.support g₂.support) :
    (g₁ + g₂).support = g₁.support g₂.support
    instance Finsupp.instAddZeroClass {ι : Type u_1} {M : Type u_3} [AddZeroClass M] :
    Equations
      noncomputable def Finsupp.addEquivFunOnFinite {M : Type u_3} [AddZeroClass M] {ι : Type u_7} [Finite ι] :
      (ι →₀ M) ≃+ (ιM)

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

      Equations
        Instances For
          noncomputable def AddEquiv.finsuppUnique {M : Type u_3} [AddZeroClass M] {ι : Type u_7} [Unique ι] :
          (ι →₀ M) ≃+ M

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

          Equations
            Instances For
              instance Finsupp.instIsCancelAdd {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [IsCancelAdd M] :
              def Finsupp.applyAddHom {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (a : ι) :
              (ι →₀ M) →+ M

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

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

              Equations
                Instances For
                  @[simp]
                  theorem Finsupp.applyAddHom_apply {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (a : ι) (g : ι →₀ M) :
                  (applyAddHom a) g = g a
                  noncomputable def Finsupp.coeFnAddHom {ι : Type u_1} {M : Type u_3} [AddZeroClass M] :
                  (ι →₀ M) →+ ιM

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

                  Equations
                    Instances For
                      @[simp]
                      theorem Finsupp.coeFnAddHom_apply {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (a✝ : ι →₀ M) (a : ι) :
                      coeFnAddHom a✝ a = a✝ a
                      theorem Finsupp.mapRange_add {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] {f : MN} {hf : f 0 = 0} (hf' : ∀ (x y : M), f (x + y) = f x + f y) (v₁ v₂ : ι →₀ M) :
                      mapRange f hf (v₁ + v₂) = mapRange f hf v₁ + mapRange f hf v₂
                      theorem Finsupp.mapRange_add' {ι : Type u_1} {F : Type u_2} {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] [FunLike F M N] [AddMonoidHomClass F M N] {f : F} (g₁ g₂ : ι →₀ M) :
                      mapRange f (g₁ + g₂) = mapRange f g₁ + mapRange f g₂
                      def Finsupp.embDomain.addMonoidHom {ι : Type u_1} {F : Type u_2} {M : Type u_3} [AddZeroClass M] (f : ι F) :
                      (ι →₀ M) →+ F →₀ M

                      Bundle Finsupp.embDomain f as an additive map from ι →₀ M to F →₀ M.

                      Equations
                        Instances For
                          @[simp]
                          theorem Finsupp.embDomain.addMonoidHom_apply {ι : Type u_1} {F : Type u_2} {M : Type u_3} [AddZeroClass M] (f : ι F) (v : ι →₀ M) :
                          @[simp]
                          theorem Finsupp.embDomain_add {ι : Type u_1} {F : Type u_2} {M : Type u_3} [AddZeroClass M] (f : ι F) (v w : ι →₀ M) :
                          embDomain f (v + w) = embDomain f v + embDomain f w
                          instance Finsupp.instNatSMul {ι : Type u_1} {M : Type u_3} [AddMonoid M] :
                          SMul (ι →₀ M)

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

                          Equations
                            instance Finsupp.instAddMonoid {ι : Type u_1} {M : Type u_3} [AddMonoid M] :
                            Equations
                              instance Finsupp.instAddCommMonoid {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] :
                              Equations
                                instance Finsupp.instNeg {ι : Type u_1} {G : Type u_5} [NegZeroClass G] :
                                Neg (ι →₀ G)
                                Equations
                                  @[simp]
                                  theorem Finsupp.coe_neg {ι : Type u_1} {G : Type u_5} [NegZeroClass G] (g : ι →₀ G) :
                                  ⇑(-g) = -g
                                  theorem Finsupp.neg_apply {ι : Type u_1} {G : Type u_5} [NegZeroClass G] (g : ι →₀ G) (a : ι) :
                                  (-g) a = -g a
                                  theorem Finsupp.mapRange_neg {ι : Type u_1} {G : Type u_5} {H : Type u_6} [NegZeroClass G] [NegZeroClass H] {f : GH} {hf : f 0 = 0} (hf' : ∀ (x : G), f (-x) = -f x) (v : ι →₀ G) :
                                  mapRange f hf (-v) = -mapRange f hf v
                                  theorem Finsupp.mapRange_neg' {ι : Type u_1} {F : Type u_2} {G : Type u_5} {H : Type u_6} [AddGroup G] [SubtractionMonoid H] [FunLike F G H] [AddMonoidHomClass F G H] {f : F} (v : ι →₀ G) :
                                  mapRange f (-v) = -mapRange f v
                                  instance Finsupp.instSub {ι : Type u_1} {G : Type u_5} [SubNegZeroMonoid G] :
                                  Sub (ι →₀ G)
                                  Equations
                                    @[simp]
                                    theorem Finsupp.coe_sub {ι : Type u_1} {G : Type u_5} [SubNegZeroMonoid G] (g₁ g₂ : ι →₀ G) :
                                    ⇑(g₁ - g₂) = g₁ - g₂
                                    theorem Finsupp.sub_apply {ι : Type u_1} {G : Type u_5} [SubNegZeroMonoid G] (g₁ g₂ : ι →₀ G) (a : ι) :
                                    (g₁ - g₂) a = g₁ a - g₂ a
                                    theorem Finsupp.mapRange_sub {ι : Type u_1} {G : Type u_5} {H : Type u_6} [SubNegZeroMonoid G] [SubNegZeroMonoid H] {f : GH} {hf : f 0 = 0} (hf' : ∀ (x y : G), f (x - y) = f x - f y) (v₁ v₂ : ι →₀ G) :
                                    mapRange f hf (v₁ - v₂) = mapRange f hf v₁ - mapRange f hf v₂
                                    theorem Finsupp.mapRange_sub' {ι : Type u_1} {F : Type u_2} {G : Type u_5} {H : Type u_6} [AddGroup G] [SubtractionMonoid H] [FunLike F G H] [AddMonoidHomClass F G H] {f : F} (v₁ v₂ : ι →₀ G) :
                                    mapRange f (v₁ - v₂) = mapRange f v₁ - mapRange f v₂
                                    instance Finsupp.instIntSMul {ι : Type u_1} {G : Type u_5} [AddGroup G] :
                                    SMul (ι →₀ G)

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

                                    Equations
                                      instance Finsupp.instAddGroup {ι : Type u_1} {G : Type u_5} [AddGroup G] :
                                      Equations
                                        instance Finsupp.instAddCommGroup {ι : Type u_1} {G : Type u_5} [AddCommGroup G] :
                                        Equations
                                          @[simp]
                                          theorem Finsupp.support_neg {ι : Type u_1} {G : Type u_5} [AddGroup G] (f : ι →₀ G) :
                                          theorem Finsupp.support_sub {ι : Type u_1} {G : Type u_5} [DecidableEq ι] [AddGroup G] {f g : ι →₀ G} :