OAI/NumberTheory/Ostmann/QuadraticSieveDualReindex.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.QuadraticSieve.summable_dual_jacobi_seriesline 10 - theorem
OAI.Ostmann.QuadraticSieve.jacobi_signed_square_factorline 19 - theorem
OAI.Ostmann.QuadraticSieve.tsum_signed_jacobi_square_eq_dualSquareSumline 27 - theorem
OAI.Ostmann.QuadraticSieve.summable_dual_jacobi_pairsline 44 - theorem
OAI.Ostmann.QuadraticSieve.summable_dualSquareSum_termsline 51 - theorem
OAI.Ostmann.QuadraticSieve.dual_jacobi_series_eq_signed_dualSquareSumline 60