# Additive monoid structure on `ι →₀ M` #

source
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
source
def Finsupp.mapRange.zeroHom {ι : Type u_1} {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] (f : ZeroHom M N) :
ZeroHom (ι →₀ M) (ι →₀ N)

Composition with a fixed zero-preserving homomorphism is itself a zero-preserving homomorphism on functions.

Equations

- Finsupp.mapRange.zeroHom f = { toFun := Finsupp.mapRange ⇑f ⋯, map_zero' := ⋯ }

Instances For

source
@[simp]
theorem Finsupp.mapRange.zeroHom_apply {ι : Type u_1} {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] (f : ZeroHom M N) (g : ι →₀ M) :
(zeroHom f) g = mapRange ⇑f ⋯ g
source
@[simp]
theorem Finsupp.mapRange.zeroHom_id {ι : Type u_1} {M : Type u_3} [Zero M] :
zeroHom (ZeroHom.id M) = ZeroHom.id (ι →₀ M)
source
theorem Finsupp.mapRange.zeroHom_comp {ι : Type u_1} {M : Type u_3} {N : Type u_4} {O : Type u_5} [Zero M] [Zero N] [Zero O] (f : ZeroHom N O) (f₂ : ZeroHom M N) :
zeroHom (f.comp f₂) = (zeroHom f).comp (zeroHom f₂)
source
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) ⋯ }

source
@[simp]
theorem Finsupp.coe_add {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (f g : ι →₀ M) :
⇑(f + g) = ⇑f + ⇑g
source
theorem Finsupp.add_apply {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (g₁ g₂ : ι →₀ M) (a : ι) :
(g₁ + g₂) a = g₁ a + g₂ a
source
theorem Finsupp.support_add {ι : Type u_1} {M : Type u_3} [AddZeroClass M] {g₁ g₂ : ι →₀ M} [DecidableEq ι] :
(g₁ + g₂).support ⊆ g₁.support ∪ g₂.support
source
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
source
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 := ⋯ }

source
instance Finsupp.instIsLeftCancelAdd {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [IsLeftCancelAdd M] :
IsLeftCancelAdd (ι →₀ M)
source
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' := ⋯ }

Instances For

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

Instances For

source
@[simp]
theorem AddEquiv.finsuppUnique_apply {M : Type u_3} [AddZeroClass M] {ι : Type u_8} [Unique ι] (v : ι →₀ M) :
finsuppUnique v = Equiv.finsuppUnique v
source
instance Finsupp.instIsRightCancelAdd {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [IsRightCancelAdd M] :
IsRightCancelAdd (ι →₀ M)
source
instance Finsupp.instIsCancelAdd {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [IsCancelAdd M] :
IsCancelAdd (ι →₀ M)
source
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' := ⋯ }

Instances For

source
@[simp]
theorem Finsupp.applyAddHom_apply {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (a : ι) (g : ι →₀ M) :
(applyAddHom a) g = g a
source
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' := ⋯ }

Instances For

source
@[simp]
theorem Finsupp.coeFnAddHom_apply {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (a✝ : ι →₀ M) (a : ι) :
coeFnAddHom a✝ a = a✝ a
source
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₂
source
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₂
source
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' := ⋯ }

Instances For

source
@[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
source
@[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
source
@[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₂
source
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
source
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
source
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
source
theorem Finsupp.support_single_add_single {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [DecidableEq ι] {f₁ f₂ : ι} {g₁ g₂ : M} (H : f₁ ≠ f₂) (hg₁ : g₁ ≠ 0) (hg₂ : g₂ ≠ 0) :
(single f₁ g₁ + single f₂ g₂).support = {f₁, f₂}
source
theorem Finsupp.support_single_add_single_subset {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [DecidableEq ι] {f₁ f₂ : ι} {g₁ g₂ : M} :
(single f₁ g₁ + single f₂ g₂).support ⊆ {f₁, f₂}
source
theorem AddEquiv.finsuppUnique_symm {M : Type u_8} [AddZeroClass M] (d : M) :
finsuppUnique.symm d = Finsupp.single () d
source
theorem Finsupp.addCommute_iff_inter {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [DecidableEq ι] {f g : ι →₀ M} :
AddCommute f g ↔ ∀ x ∈ f.support ∩ g.support, AddCommute (f x) (g x)
source
theorem Finsupp.addCommute_of_disjoint {ι : Type u_1} {M : Type u_3} [AddZeroClass M] {f g : ι →₀ M} (h : Disjoint f.support g.support) :
AddCommute f g
source
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' := ⋯ }

Instances For

source
@[simp]
theorem Finsupp.singleAddHom_apply {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (a : ι) (b : M) :
(singleAddHom a) b = single a b
source
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
source
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
source
theorem Finsupp.update_eq_single_add {ι : Type u_1} {M : Type u_3} [AddZeroClass M] {f : ι →₀ M} {a : ι} (h : f a = 0) (b : M) :
f.update a b = single a b + f
source
theorem Finsupp.update_eq_add_single {ι : Type u_1} {M : Type u_3} [AddZeroClass M] {f : ι →₀ M} {a : ι} (h : f a = 0) (b : M) :
f.update a b = f + single a b
source
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
source
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
source
@[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'
source
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' := ⋯ }

Instances For

source
@[simp]
theorem Finsupp.eraseAddHom_apply {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (a : ι) (f : ι →₀ M) :
(eraseAddHom a) f = erase a f
source
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
source
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
source
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
source
theorem Finsupp.induction_on_max {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [LinearOrder ι] {p : (ι →₀ M) → Prop} (f : ι →₀ M) (zero : p 0) (single_add : ∀ (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.

source
theorem Finsupp.induction_on_min {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [LinearOrder ι] {p : (ι →₀ M) → Prop} (f : ι →₀ M) (zero : p 0) (single_add : ∀ (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.

source
theorem Finsupp.induction_on_max₂ {ι : Type u_1} {M : Type u_3} [AddZeroClass M] [LinearOrder ι] {p : (ι →₀ M) → Prop} (f : ι →₀ M) (zero : p 0) (add_single : ∀ (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.

source
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.

source
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 }

source
@[simp]
theorem Finsupp.coe_nsmul {ι : Type u_1} {M : Type u_3} [AddMonoid M] (n : ℕ) (f : ι →₀ M) :
⇑(n • f) = n • ⇑f
source
theorem Finsupp.nsmul_apply {ι : Type u_1} {M : Type u_3} [AddMonoid M] (n : ℕ) (f : ι →₀ M) (x : ι) :
(n • f) x = n • f x
source
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.

source
instance Finsupp.instIsAddTorsionFree {ι : Type u_1} {M : Type u_3} [AddMonoid M] [IsAddTorsionFree M] :
IsAddTorsionFree (ι →₀ M)
source
instance Finsupp.instAddCommMonoid {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] :
AddCommMonoid (ι →₀ M)
Equations

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

source
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
source
def Finsupp.mapRange.addMonoidHom {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] (f : M →+ N) :
(ι →₀ M) →+ ι →₀ N

Composition with a fixed additive homomorphism is itself an additive homomorphism on functions.

Equations

- Finsupp.mapRange.addMonoidHom f = { toFun := Finsupp.mapRange ⇑f ⋯, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem Finsupp.mapRange.addMonoidHom_apply {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] (f : M →+ N) (g : ι →₀ M) :
(addMonoidHom f) g = mapRange ⇑f ⋯ g
source
@[simp]
theorem Finsupp.mapRange.addMonoidHom_id {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] :
addMonoidHom (AddMonoidHom.id M) = AddMonoidHom.id (ι →₀ M)
source
theorem Finsupp.mapRange.addMonoidHom_comp {ι : Type u_1} {M : Type u_3} {N : Type u_4} {O : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid O] (f : N →+ O) (g : M →+ N) :
addMonoidHom (f.comp g) = (addMonoidHom f).comp (addMonoidHom g)
source
@[simp]
theorem Finsupp.mapRange.addMonoidHom_toZeroHom {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] (f : M →+ N) :
↑(addMonoidHom f) = zeroHom ↑f
source
def Finsupp.mapRange.addEquiv {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] (em' : M ≃+ N) :
(ι →₀ M) ≃+ (ι →₀ N)

`Finsupp.mapRange.AddMonoidHom` as an equiv.

Equations

- Finsupp.mapRange.addEquiv em' = { toEquiv := Finsupp.mapRange.equiv ↑em' ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem Finsupp.mapRange.addEquiv_apply {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] (em' : M ≃+ N) (g : ι →₀ M) :
(addEquiv em') g = mapRange ⇑em' ⋯ g
source
@[simp]
theorem Finsupp.mapRange.addEquiv_refl {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] :
addEquiv (AddEquiv.refl M) = AddEquiv.refl (ι →₀ M)
source
theorem Finsupp.mapRange.addEquiv_trans {ι : Type u_1} {M : Type u_3} {N : Type u_4} {O : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid O] (e₁ : M ≃+ N) (e₂ : N ≃+ O) :
addEquiv (e₁.trans e₂) = (addEquiv e₁).trans (addEquiv e₂)
source
@[simp]
theorem Finsupp.mapRange.addEquiv_symm {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] (e : M ≃+ N) :
(addEquiv e).symm = addEquiv e.symm
source
@[simp]
theorem Finsupp.mapRange.addEquiv_toAddMonoidHom {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] (e : M ≃+ N) :
↑(addEquiv e) = addMonoidHom e.toAddMonoidHom
source
@[simp]
theorem Finsupp.mapRange.addEquiv_toEquiv {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] (e : M ≃+ N) :
↑(addEquiv e) = equiv ↑e ⋯
source
instance Finsupp.instNeg {ι : Type u_1} {G : Type u_6} [NegZeroClass G] :
Neg (ι →₀ G)
Equations

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

source
@[simp]
theorem Finsupp.coe_neg {ι : Type u_1} {G : Type u_6} [NegZeroClass G] (g : ι →₀ G) :
⇑(-g) = -⇑g
source
theorem Finsupp.neg_apply {ι : Type u_1} {G : Type u_6} [NegZeroClass G] (g : ι →₀ G) (a : ι) :
(-g) a = -g a
source
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
source
instance Finsupp.instSub {ι : Type u_1} {G : Type u_6} [SubNegZeroMonoid G] :
Sub (ι →₀ G)
Equations

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

source
@[simp]
theorem Finsupp.coe_sub {ι : Type u_1} {G : Type u_6} [SubNegZeroMonoid G] (g₁ g₂ : ι →₀ G) :
⇑(g₁ - g₂) = ⇑g₁ - ⇑g₂
source
theorem Finsupp.sub_apply {ι : Type u_1} {G : Type u_6} [SubNegZeroMonoid G] (g₁ g₂ : ι →₀ G) (a : ι) :
(g₁ - g₂) a = g₁ a - g₂ a
source
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₂
source
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
source
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₂
source
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 }

source
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.

source
@[simp]
theorem Finsupp.support_neg {ι : Type u_1} {G : Type u_6} [AddGroup G] (f : ι →₀ G) :
(-f).support = f.support
source
theorem Finsupp.support_sub {ι : Type u_1} {G : Type u_6} [AddGroup G] [DecidableEq ι] {f g : ι →₀ G} :
(f - g).support ⊆ f.support ∪ g.support
source
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)
source
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
source
@[simp]
theorem Finsupp.single_neg {ι : Type u_1} {G : Type u_6} [AddGroup G] (a : ι) (b : G) :
single a (-b) = -single a b
source
@[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₂
source
@[simp]
theorem Finsupp.erase_neg {ι : Type u_1} {G : Type u_6} [AddGroup G] (a : ι) (f : ι →₀ G) :
erase a (-f) = -erase a f
source
@[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₂
source
instance Finsupp.instAddCommGroup {ι : Type u_1} {G : Type u_6} [AddCommGroup G] :
AddCommGroup (ι →₀ G)
Equations

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