Theorems · Definition · combinatorics

Finset.addConvolution

{G : Type u_1} → [AddGroup G] → [DecidableEq G] → Finset G → Finset G → G → ℕ

Given finite subsets A and B of an additive group G, convolution of A and B is a map G → ℕ that maps x ∈ G to the number of distinct representations of x in the form x = a + b, where a ∈ A, b ∈ B.

Defined in

Mathlib.Combinatorics.Additive.Convolution

Cited by

18 results in Mathlib

Foundations

Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupDecidableEq