theorem Finsupp.sum_zero' {α β γ : Type} [Zero β] [AddCommMonoid γ] [DecidableEq α] (f : α →₀ β) (g : α → β → γ) (x : α) (h : g x (f x) = 0) : f.sum g = (erase x f).sum g

theorem Finsupp.update_diff {α β : Type} [DecidableEq α] [Zero β] (f : α →₀ β) (a' : α) (b : β) (a : α) (hdif : a ≠ a') : (f.update a' b) a = f a

noncomputable def Finsupp.up {α β γ : Type} [Zero γ] (f : α →₀ β →₀ γ) (a : α) (b : β) (c : γ) : α →₀ β →₀ γ

Equations

• f.up a b c = f.update a ((f a).update b c)

theorem Finsupp.up_eq {α β γ : Type} [AddZeroClass γ] (f : α →₀ β →₀ γ) (a : α) (b : β) (c : γ) : f.up a b c = erase a f + single a ((f a).update b c)

theorem Finsupp.up_apply {α β γ : Type} [Zero γ] [DecidableEq α] [DecidableEq β] (f : α →₀ β →₀ γ) (a' : α) (b' : β) (c : γ) (a : α) (b : β) : ((f.up a' b' c) a) b = if a = a' ∧ b = b' then c else (f a) b

@[simp]

theorem Finsupp.up_diff {α β γ : Type} [DecidableEq α] [Zero γ] (f : α →₀ β →₀ γ) (a' : α) (b : β) (c : γ) (a : α) (hdif : a ≠ a') : (f.up a' b c) a = f a

@[simp]

theorem Finsupp.up_diff2 {α β γ : Type} [DecidableEq α] [DecidableEq β] [Zero γ] (f : α →₀ β →₀ γ) (a' : α) (b' : β) (c : γ) (a : α) (b : β) (hdif : b ≠ b') : ((f.up a' b' c) a) b = (f a) b

@[simp]

theorem Finsupp.up_self {α β γ : Type} [DecidableEq α] [DecidableEq β] [Zero γ] (f : α →₀ β →₀ γ) (a' : α) (b' : β) (c : γ) : ((f.up a' b' c) a') b' = c

def Finsupp.uncurried_swap {α β M : Type} [e : AddCommMonoid M] (f : α × β →₀ M) : β × α →₀ M

Equations

• f.uncurried_swap = { support := Finset.map Prod.swap_emb f.support, toFun := fun (x : β × α) => match x with | (b, a) => f (Prod.swap_emb (b, a)), mem_support_toFun := ⋯ }

theorem Finsupp.uncurried_swap_def {α β M : Type} [e : AddCommMonoid M] (f : α × β →₀ M) (x : α × β) : f.uncurried_swap x.swap = f x

theorem Finsupp.uncurried_swap_def' {α β M : Type} [e : AddCommMonoid M] (f : α × β →₀ M) (x : β × α) : f.uncurried_swap x = f x.swap

noncomputable def Finsupp.curried_swap {α β M : Type} [AddCommMonoid M] (f : α →₀ β →₀ M) : β →₀ α →₀ M

Equations

• f.curried_swap = f.uncurry.uncurried_swap.curry

theorem Finsupp.uncurry_curry2 {α β M : Type} [e : AddCommMonoid M] (f : α →₀ β →₀ M) : f.uncurry.curry = f

theorem Finsupp.uncurry_apply {α β M : Type} [e : AddCommMonoid M] (f : α →₀ β →₀ M) (a : α) (b : β) : f.uncurry (a, b) = (f a) b

theorem Finsupp.curried_swap_def {α β M : Type} [e : AddCommMonoid M] (f : α →₀ β →₀ M) (a : α) (b : β) : (f.curried_swap b) a = (f a) b

theorem Finsupp.up_swap {α β M : Type} [DecidableEq α] [DecidableEq β] [AddCommMonoid M] (f : α →₀ β →₀ M) (a' : α) (b' : β) (m : M) : (f.up a' b' m).curried_swap = f.curried_swap.up b' a' m