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 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] ↔ ∀ 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

• 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 : ι → ℕ) : ↑(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.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 : ∀ i ∈ l, 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 l' : List ι} (hl : l.Perm 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 ι} : m.Nodup → (∀ i ∈ m, s i ≠ 0) → {x : ι | x ∈ m}.Pairwise (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 : m.Nodup) (hs : ∀ i ∈ m, 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 : ∀ i ∈ t, s i ≠ 0) (pp : (↑t).Pairwise (Nat.Coprime on 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 = ⋯.mp (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 (Nat.Coprime on s)) : ↑(Nat.chineseRemainderOfFinset a s t hs pp) < ∏ i ∈ t, s i