OAI/NumberTheory/TwoPoint/Bounds/PrimeCoordinates.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The common padded prime law in the canonical finite coordinate order.

  1. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.residue_average_canonical line 19
  2. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.canonical_origin line 31