How to use chinese remainder theorem for mutliple modulos

Stream: new members

[Sham S]

lemma exists_next_a_crt (f : ℕ → ℝ)

    (hf : Filter.Tendsto f Filter.atTop Filter.atTop)

    (j prev : ℕ) :

    ∃ x : ℕ, x > prev ∧

    ∀ r < k f hf (j + 1),

    (x + (r+1)) % ((Nat.nth Nat.Prime r)^2)^2 = 0 := by

  -- Let M be the product of the moduli p_r^2.

  let M : ℕ := ∏ r ∈  Finset.range (k f hf (j+1)), (Nat.nth Nat.Prime r) ^ 2 -- symbolic

  -- Use CRT in ZMod M

  have hCRT :

    ∃ x : ℤ,

      ∀ r ∈ Finset.range (k f hf (j+1)),

        x ≡ -((r+1 : ℤ)) [ZMOD (Nat.nth Nat.Prime r)^2] :=

    by

      exact Nat.chineseRemainder_modEq_unique

I tried different ways but couldn't get to do it as these theorem applys to only two arguments

[Aaron Liu]

can you post a #mwe

[Sham S]

This is the example I'm working with. I just need to prove that

$$x \equiv \text{ r mod } (p_1 \cdots p_r)^2$$

for all

$$\forall \text{r, } 1 \leq r \leq k(j)$$

[Jakub Nowak]

Unfortunately CRT in mathlib is implemented only for Nat. I think in this case you could go around that by trying to prove something like below, or you could try to implement CRT for Ints (in which case the existing implementation for Nat might be a good start).

 have hCRT :

    ∃ x : ℕ,

      ∀ r ∈ Finset.range (k f hf (j+1)),

        x  ≡ (Nat.nth Nat.Prime r)^2 - (r+1) [MOD (Nat.nth Nat.Prime r)^2]

You can use Nat.chineseRemainderOfFinset to prove it:

have hCRT := Nat.chineseRemainderOfFinset (fun r ↦ (Nat.nth Nat.Prime r)^2 - (r + 1)) (fun r ↦ (Nat.nth Nat.Prime r) ^ 2) (Finset.range (k f hf (j+1))) ?_ ?_

[Weiyi Wang]

To be pedantic, mathlib has CRT on general CommRing docs#Ideal.quotientInfRingEquivPiQuotient, which includes Int, but I didn't check how easy it is to apply here

[Jakub Nowak]

docs#IsDedekindDomain.exists_representative_mod_finset might be easier to use.