Theorems · Definition · number theory

Finset.mulConst

{G : Type u_1} → [Group G] → [DecidableEq G] → Finset G → Finset G → ℚ≥0

The doubling constant σₘ[A, B] of two finsets A and B in a group is |A * B| / |A|. The notation σₘ[A, B] is available in scope Combinatorics.Additive.

Defined in

Mathlib.Combinatorics.Additive.DoublingConst

Cited by

18 results in Mathlib

Foundations

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

Assumes

GroupDecidableEq