OAI/NumberTheory/TotientAsymptotic/PreimageOmega.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.prime_shift_factor_count line 12

   Source documentation

   Apart from the possible prime 2, every distinct prime contributes at least one factor to the corresponding shifted-prime product.

   lemma prime_shift_factor_count {p : ℕ} (hp : p.Prime) (hne : p ≠ 2) :
       1 ≤ (p-1).primeFactorsList.length := by
   …

2. lemma OAI.TotientAsymptotic.preimage_factor_count line 21