OAI/NumberTheory/TotientAsymptotic/ProjectedCube.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Unit-box enclosure for a projected banded simplex.

  1. theorem OAI.TotientAsymptotic.projected_prime_box_enclosure line 12