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

theorem Nat.modEq_list_prod_iff {a : } {b : } {l : List } (co : List.Pairwise Nat.Coprime l) :
a b [MOD l.prod] ∀ (i : Fin l.length), a b [MOD l.get i]
theorem Nat.modEq_list_prod_iff' {ι : Type u_1} {a : } {b : } {s : ι} {l : List ι} (co : List.Pairwise (Nat.Coprime on s) l) :
a b [MOD (List.map s l).prod] il, a b [MOD s i]
def Nat.chineseRemainderOfList {ι : Type u_1} (a : ι) (s : ι) (l : List ι) :
List.Pairwise (Nat.Coprime on s) l{ k : // il, 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.

Equations
Instances For
    @[simp]
    theorem Nat.chineseRemainderOfList_nil {ι : Type u_1} (a : ι) (s : ι) :
    (Nat.chineseRemainderOfList a s [] ) = 0
    theorem Nat.chineseRemainderOfList_lt_prod {ι : Type u_1} (a : ι) (s : ι) (l : List ι) (co : List.Pairwise (Nat.Coprime on s) l) (hs : il, s i 0) :
    (Nat.chineseRemainderOfList a s l co) < (List.map s l).prod
    theorem Nat.chineseRemainderOfList_modEq_unique {ι : Type u_1} (a : ι) (s : ι) (l : List ι) (co : List.Pairwise (Nat.Coprime on s) l) {z : } (hz : il, z a i [MOD s i]) :
    z (Nat.chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
    theorem Nat.chineseRemainderOfList_perm {ι : Type u_1} (a : ι) (s : ι) {l : List ι} {l' : List ι} (hl : l.Perm l') (hs : il, s i 0) (co : List.Pairwise (Nat.Coprime on s) l) :
    def Nat.chineseRemainderOfMultiset {ι : Type u_1} (a : ι) (s : ι) {m : Multiset ι} :
    m.Nodup(∀ im, s i 0){x : ι | x m}.Pairwise (Nat.Coprime on s){ k : // im, 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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem Nat.chineseRemainderOfMultiset_lt_prod {ι : Type u_1} (a : ι) (s : ι) {m : Multiset ι} (nod : m.Nodup) (hs : im, s i 0) (pp : {x : ι | x m}.Pairwise (Nat.Coprime on s)) :
      (Nat.chineseRemainderOfMultiset a s nod hs pp) < (Multiset.map s m).prod
      def Nat.chineseRemainderOfFinset {ι : Type u_1} (a : ι) (s : ι) (t : Finset ι) (hs : it, s i 0) (pp : (↑t).Pairwise (Nat.Coprime on s)) :
      { k : // it, 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.

      Equations
      Instances For
        theorem Nat.chineseRemainderOfFinset_lt_prod {ι : Type u_1} (a : ι) (s : ι) {t : Finset ι} (hs : it, s i 0) (pp : (↑t).Pairwise (Nat.Coprime on s)) :
        (Nat.chineseRemainderOfFinset a s t hs pp) < it, s i