OAI/NumberTheory/Ostmann/QuadraticSieveNormSupport.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.QuadraticSieve.supportCoefficientsline 7 - theorem
OAI.Ostmann.QuadraticSieve.supportCoefficients_apply_memline 11 - theorem
OAI.Ostmann.QuadraticSieve.supportCoefficients_apply_not_memline 16 - theorem
OAI.Ostmann.QuadraticSieve.jacobi_sum_supportCoefficientsline 21 - theorem
OAI.Ostmann.QuadraticSieve.coefficientEnergy_supportCoefficientsline 34 - theorem
OAI.Ostmann.QuadraticSieve.jacobiEnergy_supportCoefficientsline 46 - theorem
OAI.Ostmann.QuadraticSieve.quadraticNorm_mono_columnsline 52 - theorem
OAI.Ostmann.QuadraticSieve.quadraticNorm_monoline 60