OAI/NumberTheory/TotientAsymptotic/SuffixArithmetic.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact values of the suffix data used in the collision quotient.

  1. lemma OAI.TotientAsymptotic.tupleSuffix_denominator_product line 14
  2. lemma OAI.TotientAsymptotic.tupleSuffix_denominator_eq_of_collision line 38
  3. lemma OAI.TotientAsymptotic.tupleSuffix_denominator_whole line 46
  4. lemma OAI.TotientAsymptotic.tupleSuffix_denominator_positive line 65
  5. lemma OAI.TotientAsymptotic.tupleSuffix_denominator_block line 93