OAI/NumberTheory/TotientAsymptotic/IntervalPartQuotient.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Removing the complete interval part leaves an integer sifted by that interval.

  1. lemma OAI.TotientAsymptotic.partBetween_idempotent line 11
  2. lemma OAI.TotientAsymptotic.prime_dvd_partBetween line 20
  3. lemma OAI.TotientAsymptotic.interval_part_quotient_avoids line 28
  4. lemma OAI.TotientAsymptotic.interval_part_fiber_count line 45
  5. theorem OAI.TotientAsymptotic.interval_part_fiber_bound line 74