OAI/NumberTheory/Ostmann/QuadraticSieveSignedReindexBasic.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.QuadraticSieve.OddSquarefreeIndexline 8 - def
OAI.Ostmann.QuadraticSieve.squarefreeParityMapline 10 - def
OAI.Ostmann.QuadraticSieve.squarefreeParityEquivline 15 - theorem
OAI.Ostmann.QuadraticSieve.squarefreeParityEquiv_inlline 47 - theorem
OAI.Ostmann.QuadraticSieve.squarefreeParityEquiv_inrline 50 - theorem
OAI.Ostmann.QuadraticSieve.tsum_squarefree_eq_odd_add_twiceline 55