OAI/NumberTheory/TotientAsymptotic/LocalCandidateLists.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The local normality requirements persist after every removed prefix.

  1. lemma OAI.TotientAsymptotic.candidatePrimeAt_zero line 12
  2. lemma OAI.TotientAsymptotic.candidatePrimeAt_succ line 16
  3. lemma OAI.TotientAsymptotic.candidatePrimeAt_local_normality line 21
  4. theorem OAI.TotientAsymptotic.local_normal_candidate_list_data line 36