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 Nat.Coprime l) : a ≡ b [MOD List.prod l] ↔ ∀ (i : Fin (List.length l)), a ≡ b [MOD List.get l 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.prod (List.map s l)] ↔ ∀ i ∈ l, a ≡ b [MOD s i]

def Nat.chineseRemainderOfList {ι : Type u_1} (a : ι → ℕ) (s : ι → ℕ) (l : List ι) : List.Pairwise (Nat.Coprime on 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

• One or more equations did not get rendered due to their size.
• Nat.chineseRemainderOfList a s [] x_2 = { val := 0, property := ⋯ }

@[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 : ∀ i ∈ l, s i ≠ 0) : ↑(Nat.chineseRemainderOfList a s l co) < List.prod (List.map s l)

theorem Nat.chineseRemainderOfList_modEq_unique {ι : Type u_1} (a : ι → ℕ) (s : ι → ℕ) (l : List ι) (co : List.Pairwise (Nat.Coprime on s) l) {z : ℕ} (hz : ∀ i ∈ l, z ≡ a i [MOD s i]) : z ≡ ↑(Nat.chineseRemainderOfList a s l co) [MOD List.prod (List.map s l)]

theorem Nat.chineseRemainderOfList_perm {ι : Type u_1} (a : ι → ℕ) (s : ι → ℕ) {l : List ι} {l' : List ι} (hl : List.Perm l l') (hs : ∀ i ∈ l, s i ≠ 0) (co : List.Pairwise (Nat.Coprime on s) l) : ↑(Nat.chineseRemainderOfList a s l co) = ↑(Nat.chineseRemainderOfList a s l' ⋯)

def Nat.chineseRemainderOfMultiset {ι : Type u_1} (a : ι → ℕ) (s : ι → ℕ) {m : Multiset ι} : Multiset.Nodup m → (∀ i ∈ m, s i ≠ 0) → Set.Pairwise {x : ι | x ∈ m} (Nat.Coprime on 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 : Multiset.Nodup m) (hs : ∀ i ∈ m, s i ≠ 0) (pp : Set.Pairwise {x : ι | x ∈ m} (Nat.Coprime on s)) : ↑(Nat.chineseRemainderOfMultiset a s nod hs pp) < Multiset.prod (Multiset.map s m)

def Nat.chineseRemainderOfFinset {ι : Type u_1} (a : ι → ℕ) (s : ι → ℕ) (t : Finset ι) (hs : ∀ i ∈ t, s i ≠ 0) (pp : Set.Pairwise (↑t) (Nat.Coprime on s)) : { k : ℕ // ∀ i ∈ t, k ≡ a i [MOD s i] }

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

Equations

• Nat.chineseRemainderOfFinset a s t hs pp = Eq.mp ⋯ (Nat.chineseRemainderOfMultiset a s ⋯ ⋯ ⋯)

theorem Nat.chineseRemainderOfFinset_lt_prod {ι : Type u_1} (a : ι → ℕ) (s : ι → ℕ) {t : Finset ι} (hs : ∀ i ∈ t, s i ≠ 0) (pp : Set.Pairwise (↑t) (Nat.Coprime on s)) : ↑(Nat.chineseRemainderOfFinset a s t hs pp) < Finset.prod t fun (i : ι) => s i