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

• chineseRemainderOfList: Definition of the Chinese remainder of a list

Tags

Chinese Remainder Theorem, Gödel, beta function

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]

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]

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.

Equations

• Nat.chineseRemainderOfList a s [] x_2 = ⟨0, ⋯⟩
• Nat.chineseRemainderOfList a s (i :: l) co = ⟨↑(Nat.chineseRemainder ⋯ (a i) ↑(Nat.chineseRemainderOfList a s l ⋯)), ⋯⟩

@[simp]

theorem Nat.chineseRemainderOfList_nil {ι : Type u_1} (a s : ι → ℕ) : ↑(chineseRemainderOfList a s [] ⋯) = 0

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

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]

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' ⋯)

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.

Equations

• One or more equations did not get rendered due to their size.

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

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.

Equations

• Nat.chineseRemainderOfFinset a s t hs pp = Nat.chineseRemainderOfMultiset a s ⋯ ⋯ ⋯

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