OAI/NumberTheory/TotientAsymptotic/TranslatedOrder.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Summing adjacent inversions in the translated prime-coordinate region.

  1. lemma OAI.TotientAsymptotic.finite_gap_exponential_sum line 12
  2. theorem OAI.TotientAsymptotic.translated_prefix_inversions line 38