OAI/NumberTheory/TotientAsymptotic/LocalCandidateAbundance.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual prime-product candidates retaining all local normality conditions.

  1. lemma OAI.TotientAsymptotic.local_grid_tuples_subset line 13
  2. lemma OAI.TotientAsymptotic.local_regular_tuples_subset line 20
  3. def OAI.TotientAsymptotic.localRegularCandidates line 26
  4. lemma OAI.TotientAsymptotic.local_regular_candidates_subset line 29
  5. theorem OAI.TotientAsymptotic.local_regular_candidate_abundance line 37