OAI/NumberTheory/Ostmann/QuadraticCenter/BiasSelectionQuadratic.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticCenter.quadraticReal line 16
2. lemma OAI.Ostmann.QuadraticCenter.quadraticCharacter_eq_real line 19
3. lemma OAI.Ostmann.QuadraticCenter.abs_quadraticReal_le_one line 23
4. lemma OAI.Ostmann.QuadraticCenter.norm_quadraticCharacter_le_one line 30
5. lemma OAI.Ostmann.QuadraticCenter.quadraticReal_intCast line 35
6. def OAI.Ostmann.QuadraticCenter.quadraticResidueMean line 40
7. lemma OAI.Ostmann.QuadraticCenter.translatedMean_quadratic_eq_real line 43
8. lemma OAI.Ostmann.QuadraticCenter.exists_max_quadratic_translation line 49
9. lemma OAI.Ostmann.QuadraticCenter.sum_quadraticReal_translate line 61
10. lemma OAI.Ostmann.QuadraticCenter.quadraticResidueMean_compl line 71
11. def OAI.Ostmann.QuadraticCenter.biasOrientation line 82
12. lemma OAI.Ostmann.QuadraticCenter.biasOrientation_sign line 84
13. lemma OAI.Ostmann.QuadraticCenter.biasOrientation_mul line 88