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
πŸ“ coverage
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
πŸ“ coverage
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
πŸ”Έ coverage
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
    πŸ“ coverage
    @[simp]
    theorem Nat.chineseRemainderOfList_nil {ΞΉ : Type u_1} (a s : ΞΉ β†’ β„•) :
    ↑(chineseRemainderOfList a s [] β‹―) = 0
    source
    πŸ“ coverage
    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
    πŸ“ coverage
    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
    πŸ“ coverage
    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
    πŸ”Έ coverage
    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
      πŸ“ coverage
      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
      πŸ”Έ coverage
      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
        πŸ“ coverage
        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