OAI/NumberTheory/Ostmann/Construction/InitialProductSize.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The initial product has the prescribed logarithmic size
- theorem
OAI.Ostmann.initial_product_log_errorline 12