English
The Chinese remainder for a finite set exists and is uniquely determined modulo the product of the s-values over the set.
Русский
Существование и уникальность остатка китайской теоремы для конечного множества модулей.
LaTeX
$$$\mathrm{chineseRemainderOfFinset}\ a\ s\ t\ hs\ pp$ is defined and satisfies the congruences modulo each s(i) for i ∈ t.$$
Lean4
theorem chineseRemainderOfFinset_lt_prod {t : Finset ι} (hs : ∀ i ∈ t, s i ≠ 0) (pp : Set.Pairwise t (Coprime on s)) :
chineseRemainderOfFinset a s t hs pp < ∏ i ∈ t, s i := by
simpa [chineseRemainderOfFinset] using
chineseRemainderOfMultiset_lt_prod a s t.nodup (by simpa using hs) (by simpa using pp)