OAI/NumberTheory/JointDickman/Arithmetic/SquarefreeQuotientSite.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.primeProduct_dvd_site_iff line 11
2. theorem OAI.JointDickman.coefficientPrimeSet_quotient line 23

   Source documentation

   The quotient prime set is the complementary subset when none of the selected site primes has a square dividing the original integer.

   theorem coefficientPrimeSet_quotient {B n : ℕ} {A : Finset ℕ}
       (hA : A ⊆ auxiliaryPrimes B) (ha : (∏ p ∈ A, p) ∣ n)
       (hno : ∀ p ∈ auxiliaryPrimes B, ¬ p^2 ∣ n) :
       coefficientPrimeSet B (n / (∏ p ∈ A, p)) = coefficientPrimeSet B n \ A := by
   …

   Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.coefficientPrimeSet