chineseRemainderOfFinset — Mathlib

English

The Chinese remainder for a multiset exists as a value k such that ∀ i ∈ m, k ≡ a_i (mod s_i).

Русский

Существуют k такое, что ∀ i ∈ m, k ≡ a_i (mod s_i).

LaTeX

$${ k // ∀ i ∈ m, k ≡ a_i [MOD s_i] }$$

Lean4

/-- The natural number less than `∏ i ∈ t, s i` congruent to
`a i` mod `s i` for all  `i ∈ t`. -/
def chineseRemainderOfFinset (t : Finset ι) (hs : ∀ i ∈ t, s i ≠ 0) (pp : Set.Pairwise t (Coprime on s)) :
    { k // ∀ i ∈ t, k ≡ a i [MOD s i] } := by
  simpa using chineseRemainderOfMultiset a s t.nodup (by simpa using hs) (by simpa using pp)

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