OAI/NumberTheory/TotientAsymptotic/CandidateAbundance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A positive counting-scale family of actual prime-product candidates.

  1. def OAI.TotientAsymptotic.rawCandidates line 12
  2. theorem OAI.TotientAsymptotic.raw_candidate_abundance line 15