Additive monoid structure on ι →₀ M

instance Finsupp.instAdd {ι : Type u_1} {M : Type u_3} [AddZeroClass M] : Add (ι →₀ M)

Equations

• Finsupp.instAdd = { add := Finsupp.zipWith (fun (x1 x2 : M) => x1 + x2) ⋯ }

@[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] : AddZeroClass (ι →₀ M)

Equations

• Finsupp.instAddZeroClass = { toZero := Finsupp.instZero, toAdd := Finsupp.instAdd, zero_add := ⋯, add_zero := ⋯ }

instance Finsupp.instIsLeftCancelAdd {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [IsLeftCancelAdd M] : IsLeftCancelAdd (ι →₀ M)

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

• Finsupp.addEquivFunOnFinite = { toEquiv := Finsupp.equivFunOnFinite, map_add' := ⋯ }

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

• AddEquiv.finsuppUnique = { toEquiv := Equiv.finsuppUnique, map_add' := ⋯ }

instance Finsupp.instIsRightCancelAdd {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [IsRightCancelAdd M] : IsRightCancelAdd (ι →₀ M)

instance Finsupp.instIsCancelAdd {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [IsCancelAdd 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

• Finsupp.applyAddHom a = { toFun := fun (g : ι →₀ M) => g a, map_zero' := ⋯, map_add' := ⋯ }

@[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

• Finsupp.coeFnAddHom = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }

@[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 : M → N} {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

• Finsupp.embDomain.addMonoidHom f = { toFun := fun (v : ι →₀ M) => Finsupp.embDomain f v, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Finsupp.embDomain.addMonoidHom_apply {ι : Type u_1} {F : Type u_2} {M : Type u_3} [AddZeroClass M] (f : ι ↪ F) (v : ι →₀ M) : (addMonoidHom f) v = embDomain f v

@[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

• Finsupp.instNatSMul = { smul := fun (n : ℕ) (v : ι →₀ M) => Finsupp.mapRange (fun (x : M) => n • x) ⋯ v }

instance Finsupp.instAddMonoid {ι : Type u_1} {M : Type u_3} [AddMonoid M] : AddMonoid (ι →₀ M)

Equations

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

instance Finsupp.instAddCommMonoid {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] : AddCommMonoid (ι →₀ M)

Equations

• Finsupp.instAddCommMonoid = { toAddMonoid := Finsupp.instAddMonoid, add_comm := ⋯ }

instance Finsupp.instNeg {ι : Type u_1} {G : Type u_5} [NegZeroClass G] : Neg (ι →₀ G)

Equations

• Finsupp.instNeg = { neg := Finsupp.mapRange Neg.neg ⋯ }

@[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 : G → H} {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

• Finsupp.instSub = { sub := Finsupp.zipWith Sub.sub ⋯ }

@[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 : G → H} {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

• Finsupp.instIntSMul = { smul := fun (n : ℤ) (v : ι →₀ G) => Finsupp.mapRange (fun (x : G) => n • x) ⋯ v }

instance Finsupp.instAddGroup {ι : Type u_1} {G : Type u_5} [AddGroup G] : AddGroup (ι →₀ G)

Equations

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

instance Finsupp.instAddCommGroup {ι : Type u_1} {G : Type u_5} [AddCommGroup G] : AddCommGroup (ι →₀ G)

Equations

• Finsupp.instAddCommGroup = { toAddGroup := Finsupp.instAddGroup, add_comm := ⋯ }

@[simp]

theorem Finsupp.support_neg {ι : Type u_1} {G : Type u_5} [AddGroup G] (f : ι →₀ G) : (-f).support = f.support

theorem Finsupp.support_sub {ι : Type u_1} {G : Type u_5} [DecidableEq ι] [AddGroup G] {f g : ι →₀ G} : (f - g).support ⊆ f.support ∪ g.support