OAI/NumberTheory/TwoPoint/Bounds/AmbientLitOrigin.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Lit consistency in the full prime pool supplies the common tuple-column origins.

  1. theorem OAI.TwoPointCorrelations.ambient_lit_common_origin line 13
  2. theorem OAI.TwoPointCorrelations.ambient_tuple_lit_origin line 24