OAI/NumberTheory/Ostmann/QuadraticSieveSignedReindex.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.QuadraticSieve.tsum_positive_eq_odd_square_twiceline 7 - theorem
OAI.Ostmann.QuadraticSieve.tsum_positive_signed_eq_odd_square_twiceline 21 - theorem
OAI.Ostmann.QuadraticSieve.signed_squarefree_pair_injectiveline 45 - theorem
OAI.Ostmann.QuadraticSieve.summable_signed_squarefree_pairsline 58 - theorem
OAI.Ostmann.QuadraticSieve.tsum_int_eq_zero_add_signed_squarefreeline 64