OAI/NumberTheory/TotientAsymptotic/NormalTotientBands.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Normal prime divisors of a preimage force many factors in its totient bands.

  1. lemma OAI.TotientAsymptotic.omegaIn_dvd line 11
  2. lemma OAI.TotientAsymptotic.shifted_prime_product_dvd_totient line 18
  3. lemma OAI.TotientAsymptotic.normal_prime_totient_band_lower line 26
  4. lemma OAI.TotientAsymptotic.omegaIn_partBetween line 44
  5. lemma OAI.TotientAsymptotic.normal_prime_interval_part_lower line 59