OAI/NumberTheory/Ostmann/QuadraticSieveLeadingCorrelations.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.QuadraticSieve.dualLeadingCorrelationline 9 - def
OAI.Ostmann.QuadraticSieve.complementLeadingCorrelationline 16 - theorem
OAI.Ostmann.QuadraticSieve.dualLeadingCorrelation_eqline 23 - theorem
OAI.Ostmann.QuadraticSieve.complementLeadingCorrelation_eqline 35