OAI/NumberTheory/TotientAsymptotic/CommonPrimeMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The reciprocal mass after one common largest prime has been extracted.

  1. abbrev OAI.TotientAsymptotic.PairedFactors line 11
  2. def OAI.TotientAsymptotic.pairedProduct line 13
  3. structure OAI.TotientAsymptotic.CommonPrimeWitness line 15
  4. lemma OAI.TotientAsymptotic.common_prime_fiber_sum line 27
  5. lemma OAI.TotientAsymptotic.common_prime_fiber_bound line 42
  6. theorem OAI.TotientAsymptotic.common_prime_mass_bound line 74