OAI/NumberTheory/Ostmann/QuadraticSieveSquareRemoval.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.QuadraticSieve.jacobi_square_mul_leftline 7 - theorem
OAI.Ostmann.QuadraticSieve.jacobi_square_mul_rightline 15 - def
OAI.Ostmann.QuadraticSieve.gcdReducedModulusline 24 - theorem
OAI.Ostmann.QuadraticSieve.mul_eq_gcd_sq_mul_reducedline 27 - theorem
OAI.Ostmann.QuadraticSieve.jacobi_gcd_denominatorline 37 - theorem
OAI.Ostmann.QuadraticSieve.gcdReducedModulus_squarefreeline 49