OAI/NumberTheory/Ostmann/QuadraticSieveTotientRows.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.QuadraticSieve.totientCoefficientsline 9 - theorem
OAI.Ostmann.QuadraticSieve.coefficientEnergy_totient_leline 12 - def
OAI.Ostmann.QuadraticSieve.coprimeTotientJacobiRowline 28 - theorem
OAI.Ostmann.QuadraticSieve.coprimeTotientJacobiRow_eqline 33 - theorem
OAI.Ostmann.QuadraticSieve.totient_mainConvolution_difference_boundline 49