OAI/NumberTheory/TotientAsymptotic/FailedRowPrefix.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual prime prefix before a first failed row belongs to the unbanded simplex.

  1. lemma OAI.TotientAsymptotic.fordRowSum_truncate line 11
  2. lemma OAI.TotientAsymptotic.rows_give_enlarged_prefix line 21
  3. def OAI.TotientAsymptotic.fordPrefixPrimes line 39
  4. theorem OAI.TotientAsymptotic.failed_row_prefix_conditions line 41