finsupp α β, denoted α →₀ β, is the type of functions f : α → β such that f x = 0 for all but finitely many x.

single a b is the finitely supported function which has value b at a and zero otherwise.

on_finset s f hf is the finsupp function representing f restricted to the set s. The function needs to be 0 outside of s. Use this when the set needs filtered anyway, otherwise often better set representation is available.

The composition of f : β₁ → β₂ and g : α →₀ β₁ is map_range f hf g : α →₀ β₂, well defined when f 0 = 0.

Given f : α₁ ↪ α₂ and v : α₁ →₀ β, emb_domain f v : α₂ →₀ β is the finitely supported function whose value at f a : α₂ is v a. For a b : α₂ outside the range of f it is zero.

zip_with f hf g₁ g₂ is the finitely supported function satisfying zip_with f hf g₁ g₂ a = f (g₁ a) (g₂ a), and well defined when f 0 0 = 0.

sum f g is the sum of g a (f a) over the support of f.

prod f g is the product of g a (f a) over the support of f.

Given f : α₁ → α₂ and v : α₁ →₀ β, map_domain f v : α₂ →₀ β is the finitely supported function whose value at a : α₂ is the sum of v x over all x such that f x = a.

The product of f g : α →₀ β is the finitely supported function whose value at a is the sum of f x * g y over all pairs x, y such that x + y = a. (Think of the product of multivariate polynomials where α is the monoid of monomial exponents.)

The unit of the multiplication is single 0 1, i.e. the function that is 1 at 0 and zero elsewhere.

filter p f is the function which is f a if p a is true and 0 otherwise.

subtype_domain p f is the restriction of the finitely supported function f to the subtype p.

The order on σ →₀ ℕ is well-founded.