OAI/NumberTheory/TotientAsymptotic/InitialRoughData.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact sieve data supplied by extraction from the initial rough factor.

  1. structure OAI.TotientAsymptotic.InitialPrimeData line 9
  2. lemma OAI.TotientAsymptotic.initial_rough_sieve_data line 22