structure CoveringSystem (R : Type u_1) [CommSemiring R] : Type (max 1 u_1)

A covering system of a semiring R is a finite set of cosets of non-zero ideals whose union covers the whole ring. In the case where R = ℤ, this corresponds to a choice of finitely many congruence relations such that every integer satisfies at least one of the relations.

• ι : Type
• fintypeIndex : Fintype self.ι
• residue : self.ι → R
• moduli : self.ι → Ideal R
• unionCovers : ⋃ (i : self.ι), {self.residue i} + ↑(self.moduli i) = Set.univ
• non_trivial (i : self.ι) : self.moduli i ≠ ⊥

structure StrictCoveringSystem (R : Type u_1) [CommSemiring R] extends CoveringSystem R : Type (max 1 u_1)

We say a covering system is strict if all the congruence relations that define it are take modulo a different ideal (or number).

Note: this corresponds to the notion of a covering system that Erdos was using in [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

• ι : Type
• fintypeIndex : Fintype self.ι
• residue : self.ι → R
• moduli : self.ι → Ideal R
• unionCovers : ⋃ (i : self.ι), {self.residue i} + ↑(self.moduli i) = Set.univ
• non_trivial (i : self.ι) : self.moduli i ≠ ⊥
• injective_moduli : Function.Injective self.moduli

def CoveringSystem.coset {R : Type u_1} [CommSemiring R] (c : CoveringSystem R) (i : c.ι) : Set R

Equations

• c.coset i = {c.residue i} + ↑(c.moduli i)

@[simp]

theorem CoveringSystem.iUnion_cosets {R : Type u_1} [CommSemiring R] (c : CoveringSystem R) : ⋃ (i : c.ι), c.coset i = Set.univ