Covering systems

Covering and exact covering systems of residue classes, minimum moduli, Erdős–Graham and Fraenkel-type results.

StructureCovering system#✓fully proved

A covering system of a commutative semiring \(R\) is a finite family of cosets \(r_i + I_i = \{r_i + a : a \in I_i\}\), where each \(I_i\) is an ideal of \(R\) different from both \(\{0\}\) and \(R\), whose union is all of \(R\). In the case \(R = \mathbb{Z}\), this corresponds to a choice of finitely many congruences \(x \equiv r_i \pmod{n_i}\) with moduli \(n_i \ge 2\) such that every integer satisfies at least one of them.

structure CoveringSystem (R : Type*) [CommSemiring R] where
  ι : Type
  [fintypeIndex : Fintype ι]
  residue : ι → R
  moduli : ι → Ideal R
  unionCovers : ⋃ i, ({residue i} : Set R) + (moduli i : Set R) = @Set.univ R
  ne_bot : ∀ i, moduli i ≠ ⊥
  ne_top : ∀ i, moduli i ≠ ⊤

Used by 1

Used byStrict covering system

StructureStrict covering system#✓fully proved

A covering system of a commutative semiring \(R\), given by cosets \(r_i + I_i\), is strict if the ideals \(I_i\) are pairwise distinct. In the case \(R = \mathbb{Z}\), this means that the congruences defining it have pairwise distinct moduli.

This corresponds to the notion of covering system that Erdős and Graham use.

structure StrictCoveringSystem (R : Type*) [CommSemiring R] extends CoveringSystem R where
  injective_moduli : moduli.Injective

Sources

• [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

Uses 1

Statement usesCovering system

• A question of Erdős and Graham on covering systems
• Exact covering system digraphs
• Exact covering systems
• Minimum modulus of covering systems

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.