Theorems · Definition · number theory

Finset.subConst

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

The difference 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