Theorems · Definition · combinatorics

Finset.convolution

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

Given finite subsets A and B of a 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 = ab, where a ∈ A, b ∈ B.

Defined in

Mathlib.Combinatorics.Additive.Convolution

Cited by

20 results in Mathlib

Foundations

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

Assumes

GroupDecidableEq