Mathlib Phrasebook

1.1. Sets🔗

1.1.1. Sets and finite sets🔗

The basic objects of study in additive combinatorics are "additive sets", i.e. sets in a group. Sets in Mathlib live on a single type. Here is how to declare a subset of an abelian group:

variable {G : Type*} [AddCommGroup G] {A : Set G}

Finite sets can be represented in two ways. Either we work with sets that happen to be finite:

variable {A : Set G} (hA : A.Finite)

or we work with bundled finite sets

variable {A : Finset G}

The latter is preferred in Mathlib since it gives access to e.g. Finset.sum.

In finite groups, all sets are finite and therefore all sets happen to be finite. We tend to prefer working with Finset anyway to access its API.

The cardinality of a Set is Set.ncard:

variable {A : Set G} A.ncard : ℕ#check A.ncard 
A.ncard : ℕ

Similarly, the cardinality of a Finset is Finset.card. We provide the usual cardinality notation for it:

variable {A : Finset G} open scoped Finset #A : ℕ#check #A 
#A : ℕ

1.1.2. Indicators🔗

The R-valued indicator function of (A : Set G) is written as

variable {R : Type*} [Zero R] [One R] {A : Set G} A.indicator 1 : G → R#check A.indicator (1 : G → R) 
A.indicator 1 : G → R

AddCombi provides convenient notation:

open scoped Indicator 𝟭_[A, R] : G → R#check 𝟭_[A, R] 
𝟭_[A, R] : G → R

When no return type is specified, the notation defaults to the ℕ-valued indicator.

𝟭_[A] : G → ℕ#check 𝟭_[A] 
𝟭_[A] : G → ℕ

When talking about the indicator function of a Finset, you might need to help Lean somewhat using a type ascription. In the following, g has type G, so Lean coerces A to Set G.

variable {A : Finset G} {g : G} 𝟭_[↑A] g : ℕ#check 𝟭_[A] g

Without such unification information, a type ascription is required.

𝟭_[↑A] : G → ℕ#check 𝟭_[(A : Set G)]

1.1.3. Sumsets🔗

Sumsets and product sets in an (additive) monoid enjoy the usual arithmetic notation, once the Pointwise scope is opened:

variable {A B : Set ℕ} open scoped Pointwise A + B : Set ℕ#check A + B A * B : Set ℕ#check A * B 
A + B : Set ℕ
A * B : Set ℕ

Similarly, the notations for repeated sumsets and product sets is simply

variable {n : ℕ} n • A : Set ℕ#check n • A A ^ n : Set ℕ#check A ^ n 
n • A : Set ℕ
A ^ n : Set ℕ

Careful! In additive combinatorics one also encounters the "dilate set", where each element of the set is multiplied by a fixed natural number. We currently do not provide a way to write this operation conveniently. Dilation by anything other than a natural number uses the standard scalar multiplication notation:

variable {A : Set ℝ} {q : ℚ} q • A : Set ℝ#check q • A 
q • A : Set ℝ

Sets can also be pointwise negated or inverted (with the usual convention that (0 : Set G₀)⁻¹ = 0):

A⁻¹ : Set ℝ#check A⁻¹ -A : Set ℝ#check -A 
A⁻¹ : Set ℝ
-A : Set ℝ

Finally, Finset is equipped with the same operations under the further assumption that the group has decidable equality:

variable {G : Type*} [AddCommGroup G] [DecidableEq G] {A B : Finset G} A + B : Finset G#check A + B 
A + B : Finset G

This extra assumption allows us to perform computations with Finset:

{5, 8, 6, 9}#eval ({1, 2} + {4, 7} : Finset ℕ) 
{5, 8, 6, 9}