Additive monoid structure on ι →₀ M

theorem Finsupp.apply_single {ι : Type u_1} {F : Type u_2} {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] [FunLike F M N] [ZeroHomClass F M N] (e : F) (i : ι) (m : M) (b : ι) : e ((single i m) b) = (single i (e m)) b

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_8} [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_8} [Unique ι] : (ι →₀ M) ≃+ M

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

Equations

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

@[simp]

theorem AddEquiv.finsuppUnique_apply {M : Type u_3} [AddZeroClass M] {ι : Type u_8} [Unique ι] (v : ι →₀ M) : finsuppUnique v = Equiv.finsuppUnique v

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

@[simp]

theorem Finsupp.single_add {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (a : ι) (b₁ b₂ : M) : single a (b₁ + b₂) = single a b₁ + single a b₂

theorem Finsupp.single_add_apply {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (a : ι) (m₁ m₂ : M) (b : ι) : (single a (m₁ + m₂)) b = (single a m₁) b + (single a m₂) b

theorem Finsupp.support_single_add {ι : Type u_1} {M : Type u_3} [AddZeroClass M] {a : ι} {b : M} {f : ι →₀ M} (ha : a ∉ f.support) (hb : b ≠ 0) : (single a b + f).support = Finset.cons a f.support ha

theorem Finsupp.support_add_single {ι : Type u_1} {M : Type u_3} [AddZeroClass M] {a : ι} {b : M} {f : ι →₀ M} (ha : a ∉ f.support) (hb : b ≠ 0) : (f + single a b).support = Finset.cons a f.support ha

theorem AddEquiv.finsuppUnique_symm {M : Type u_8} [AddZeroClass M] (d : M) : finsuppUnique.symm d = Finsupp.single () d

def Finsupp.singleAddHom {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (a : ι) : M →+ ι →₀ M

Finsupp.single as an AddMonoidHom.

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

Equations

• Finsupp.singleAddHom a = { toFun := Finsupp.single a, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Finsupp.singleAddHom_apply {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (a : ι) (b : M) : (singleAddHom a) b = single a b

theorem Finsupp.update_eq_single_add_erase {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (f : ι →₀ M) (a : ι) (b : M) : f.update a b = single a b + erase a f

theorem Finsupp.update_eq_erase_add_single {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (f : ι →₀ M) (a : ι) (b : M) : f.update a b = erase a f + single a b

theorem Finsupp.single_add_erase {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (a : ι) (f : ι →₀ M) : single a (f a) + erase a f = f

theorem Finsupp.erase_add_single {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (a : ι) (f : ι →₀ M) : erase a f + single a (f a) = f

@[simp]

theorem Finsupp.erase_add {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (a : ι) (f f' : ι →₀ M) : erase a (f + f') = erase a f + erase a f'

def Finsupp.eraseAddHom {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (a : ι) : (ι →₀ M) →+ ι →₀ M

Finsupp.erase as an AddMonoidHom.

Equations

• Finsupp.eraseAddHom a = { toFun := Finsupp.erase a, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Finsupp.eraseAddHom_apply {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (a : ι) (f : ι →₀ M) : (eraseAddHom a) f = erase a f

theorem Finsupp.induction {ι : Type u_1} {M : Type u_3} [AddZeroClass M] {motive : (ι →₀ M) → Prop} (f : ι →₀ M) (zero : motive 0) (single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)) : motive f

theorem Finsupp.induction₂ {ι : Type u_1} {M : Type u_3} [AddZeroClass M] {motive : (ι →₀ M) → Prop} (f : ι →₀ M) (zero : motive 0) (add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (f + single a b)) : motive f

theorem Finsupp.induction_linear {ι : Type u_1} {M : Type u_3} [AddZeroClass M] {motive : (ι →₀ M) → Prop} (f : ι →₀ M) (zero : motive 0) (add : ∀ (f g : ι →₀ M), motive f → motive g → motive (f + g)) (single : ∀ (a : ι) (b : M), motive (single a b)) : motive f

theorem Finsupp.induction_on_max {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [LinearOrder ι] {p : (ι →₀ M) → Prop} (f : ι →₀ M) (h0 : p 0) (ha : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (single a b + f)) : p f

A finitely supported function can be built by adding up single a b for increasing a.

The lemma induction_on_max₂ swaps the argument order in the sum.

theorem Finsupp.induction_on_min {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [LinearOrder ι] {p : (ι →₀ M) → Prop} (f : ι →₀ M) (h0 : p 0) (ha : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, a < c) → b ≠ 0 → p f → p (single a b + f)) : p f

A finitely supported function can be built by adding up single a b for decreasing a.

The lemma induction_on_min₂ swaps the argument order in the sum.

theorem Finsupp.induction_on_max₂ {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [LinearOrder ι] {p : (ι →₀ M) → Prop} (f : ι →₀ M) (h0 : p 0) (ha : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)) : p f

A finitely supported function can be built by adding up single a b for increasing a.

The lemma induction_on_max swaps the argument order in the sum.

theorem Finsupp.induction_on_min₂ {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [LinearOrder ι] {p : (ι →₀ M) → Prop} (f : ι →₀ M) (h0 : p 0) (ha : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, a < c) → b ≠ 0 → p f → p (f + single a b)) : p f

A finitely supported function can be built by adding up single a b for decreasing a.

The lemma induction_on_min swaps the argument order in the sum.

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 := ⋯ }

theorem Finsupp.single_add_single_eq_single_add_single {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] {k l m n : ι} {u v : M} (hu : u ≠ 0) (hv : v ≠ 0) : single k u + single l v = single m u + single n v ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n

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

Equations

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

@[simp]

theorem Finsupp.coe_neg {ι : Type u_1} {G : Type u_6} [NegZeroClass G] (g : ι →₀ G) : ⇑(-g) = -⇑g

theorem Finsupp.neg_apply {ι : Type u_1} {G : Type u_6} [NegZeroClass G] (g : ι →₀ G) (a : ι) : (-g) a = -g a

theorem Finsupp.mapRange_neg {ι : Type u_1} {G : Type u_6} {H : Type u_7} [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

instance Finsupp.instSub {ι : Type u_1} {G : Type u_6} [SubNegZeroMonoid G] : Sub (ι →₀ G)

Equations

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

@[simp]

theorem Finsupp.coe_sub {ι : Type u_1} {G : Type u_6} [SubNegZeroMonoid G] (g₁ g₂ : ι →₀ G) : ⇑(g₁ - g₂) = ⇑g₁ - ⇑g₂

theorem Finsupp.sub_apply {ι : Type u_1} {G : Type u_6} [SubNegZeroMonoid G] (g₁ g₂ : ι →₀ G) (a : ι) : (g₁ - g₂) a = g₁ a - g₂ a

theorem Finsupp.mapRange_sub {ι : Type u_1} {G : Type u_6} {H : Type u_7} [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_neg' {ι : Type u_1} {F : Type u_2} {G : Type u_6} {H : Type u_7} [AddGroup G] [SubtractionMonoid H] [FunLike F G H] [AddMonoidHomClass F G H] {f : F} (v : ι →₀ G) : mapRange ⇑f ⋯ (-v) = -mapRange ⇑f ⋯ v

theorem Finsupp.mapRange_sub' {ι : Type u_1} {F : Type u_2} {G : Type u_6} {H : Type u_7} [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_6} [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_6} [AddGroup G] : AddGroup (ι →₀ G)

Equations

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

@[simp]

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

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

theorem Finsupp.erase_eq_sub_single {ι : Type u_1} {G : Type u_6} [AddGroup G] (f : ι →₀ G) (a : ι) : erase a f = f - single a (f a)

theorem Finsupp.update_eq_sub_add_single {ι : Type u_1} {G : Type u_6} [AddGroup G] (f : ι →₀ G) (a : ι) (b : G) : f.update a b = f - single a (f a) + single a b

@[simp]

theorem Finsupp.single_neg {ι : Type u_1} {G : Type u_6} [AddGroup G] (a : ι) (b : G) : single a (-b) = -single a b

@[simp]

theorem Finsupp.single_sub {ι : Type u_1} {G : Type u_6} [AddGroup G] (a : ι) (b₁ b₂ : G) : single a (b₁ - b₂) = single a b₁ - single a b₂

@[simp]

theorem Finsupp.erase_neg {ι : Type u_1} {G : Type u_6} [AddGroup G] (a : ι) (f : ι →₀ G) : erase a (-f) = -erase a f

@[simp]

theorem Finsupp.erase_sub {ι : Type u_1} {G : Type u_6} [AddGroup G] (a : ι) (f₁ f₂ : ι →₀ G) : erase a (f₁ - f₂) = erase a f₁ - erase a f₂

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

Equations

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