Documentation

Mathlib.Data.Nat.ChineseRemainder

Chinese Remainder Theorem #

This file provides definitions and theorems for the Chinese Remainder Theorem. These are used in Gödel's Beta function, which is used in proving Gödel's incompleteness theorems.

Main result #

Tags #

Chinese Remainder Theorem, Gödel, beta function

source
theorem Nat.modEq_list_prod_iff {a b : ℕ} {l : List ℕ} (co : List.Pairwise Coprime l) :
a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
source
theorem Nat.modEq_list_map_prod_iff {ι : Type u_1} {a b : ℕ} {s : ι → ℕ} {l : List ι} (co : List.Pairwise (Function.onFun Coprime s) l) :
a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i]
source
def Nat.chineseRemainderOfList {ι : Type u_1} (a s : ι → ℕ) (l : List ι) :
List.Pairwise (Function.onFun Coprime s) l → { k : ℕ // ∀ i ∈ l, k ≡ a i [MOD s i] }

The natural number less than (l.map s).prod congruent to a i mod s i for all i ∈ l.

Instances For
    source
    @[simp]
    theorem Nat.chineseRemainderOfList_nil {ι : Type u_1} (a s : ι → ℕ) :
    ↑(chineseRemainderOfList a s [] ⋯) = 0
    source
    theorem Nat.chineseRemainderOfList_lt_prod {ι : Type u_1} (a s : ι → ℕ) (l : List ι) (co : List.Pairwise (Function.onFun Coprime s) l) (hs : ∀ i ∈ l, s i ≠ 0) :
    ↑(chineseRemainderOfList a s l co) < (List.map s l).prod
    source
    theorem Nat.chineseRemainderOfList_modEq_unique {ι : Type u_1} (a s : ι → ℕ) (l : List ι) (co : List.Pairwise (Function.onFun Coprime s) l) {z : ℕ} (hz : ∀ i ∈ l, z ≡ a i [MOD s i]) :
    z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
    source
    theorem Nat.chineseRemainderOfList_perm {ι : Type u_1} (a s : ι → ℕ) {l l' : List ι} (hl : l.Perm l') (hs : ∀ i ∈ l, s i ≠ 0) (co : List.Pairwise (Function.onFun Coprime s) l) :
    ↑(chineseRemainderOfList a s l co) = ↑(chineseRemainderOfList a s l' ⋯)
    source
    def Nat.chineseRemainderOfMultiset {ι : Type u_1} (a s : ι → ℕ) {m : Multiset ι} :
    m.Nodup → (∀ i ∈ m, s i ≠ 0) → {x : ι | x ∈ m}.Pairwise (Function.onFun Coprime s) → { k : ℕ // ∀ i ∈ m, k ≡ a i [MOD s i] }

    The natural number less than (m.map s).prod congruent to a i mod s i for all i ∈ m.

    Instances For
      source
      theorem Nat.chineseRemainderOfMultiset_lt_prod {ι : Type u_1} (a s : ι → ℕ) {m : Multiset ι} (nod : m.Nodup) (hs : ∀ i ∈ m, s i ≠ 0) (pp : {x : ι | x ∈ m}.Pairwise (Function.onFun Coprime s)) :
      ↑(chineseRemainderOfMultiset a s nod hs pp) < (Multiset.map s m).prod
      source
      def Nat.chineseRemainderOfFinset {ι : Type u_1} (a s : ι → ℕ) (t : Finset ι) (hs : ∀ i ∈ t, s i ≠ 0) (pp : (↑t).Pairwise (Function.onFun 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.

      Instances For
        source
        theorem Nat.chineseRemainderOfFinset_lt_prod {ι : Type u_1} (a s : ι → ℕ) {t : Finset ι} (hs : ∀ i ∈ t, s i ≠ 0) (pp : (↑t).Pairwise (Function.onFun Coprime s)) :
        ↑(chineseRemainderOfFinset a s t hs pp) < ∏ i ∈ t, s i