Theorems · Definition · number theory

Nat.chineseRemainderOfFinset

{ι : Type u_1} →
  (a s : ι → ℕ) →
    (t : Finset ι) →
      (∀ i ∈ t, s i ≠ 0) → (↑t).Pairwise (Function.onFun Nat.Coprime s) → { k // ∀ i ∈ t, k ≡ a i [MOD s i] }

The natural number less than ∏ i ∈ t, s i congruent to a i mod s i for all i ∈ t.

Defined in

Mathlib.Data.Nat.ChineseRemainder

Cited by

3 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound