OAI/NumberTheory/Ostmann/Construction/FavorableGiantCutoff.lean
1 declarations, 0 contain sorry, 0 declared as axioms
A selected favorable block lies below the endpoint-test prime cutoff
- theorem
OAI.Ostmann.eventual_favorable_giant_cutoffline 9