OAI/NumberTheory/Ostmann/Construction/FavorableBlockSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Selecting one dense logarithmic block from the favorable prime mass

  1. theorem OAI.Ostmann.favorable_logarithmic_block line 10