chineseRemainderOfFinset_lt_prod — Mathlib

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)

Похожие утверждения