OAI/NumberTheory/Ostmann/Arithmetic/MovingArithmeticModulus.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingArithmeticModuli_ne_zero line 10
2. theorem OAI.Ostmann.movingArithmeticModuli_coprime line 19
3. theorem OAI.Ostmann.movingArithmeticModuli_periods line 45

   Source documentation

   The three arithmetic periods divide the concrete CRT modulus.

   theorem movingArithmeticModuli_periods {I : Type*} (r : ℕ) (q : I → ℕ)
       (P : Finset ℕ) (S : Finset I) (R : ℤ) (k : ℕ) (hR : R ^ k ∣ (r : ℤ)) :
       (R ^ k ∣ ((∏ b, movingArithmeticModuli r q P S b : ℕ) : ℤ)) ∧
       (∀ p ∈ P, (p ^ 2 : ℤ) ∣ ((∏ b, movingArithmeticModuli r q P S b : ℕ) : ℤ)) ∧
       (∀ i ∈ S, (q i : ℤ) ∣ ((∏ b, movingArithmeticModuli r q P S b : ℕ) : ℤ)) := by
   …

   Mentions: OAI.Ostmann.movingArithmeticModuli