Theorems · Definition · number theory

Finset.addConst

{G : Type u_1} → [AddGroup 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

17 results in Mathlib

Foundations

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

Assumes

AddGroupDecidableEq