OAI/NumberTheory/TotientAsymptotic/CandidateProperties.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic and size properties of the actual counted candidates.

  1. theorem OAI.TotientAsymptotic.raw_candidate_prime_data line 13
  2. theorem OAI.TotientAsymptotic.raw_candidate_ratio_bound line 39
  3. theorem OAI.TotientAsymptotic.raw_candidate_size_data line 49