OAI/NumberTheory/Ostmann/QuadraticSieveGauss.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.QuadraticSieve.fourier_div_eq_stdAddChar_mulline 7 - theorem
OAI.Ostmann.QuadraticSieve.sum_fin_residues_eq_sum_zmodline 15 - theorem
OAI.Ostmann.QuadraticSieve.jacobi_gauss_mulShiftline 25 - theorem
OAI.Ostmann.QuadraticSieve.finite_jacobi_gauss_transformline 33 - theorem
OAI.Ostmann.QuadraticSieve.jacobi_dftline 56