OAI/NumberTheory/Ostmann/QuadraticCenter/QuadraticBiasLittleOBasic.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticCenter.quadraticBiasValue line 12
2. lemma OAI.Ostmann.QuadraticCenter.quadraticBiasValue_prime line 18
3. lemma OAI.Ostmann.QuadraticCenter.quadraticBiasValue_nonneg line 23
4. lemma OAI.Ostmann.QuadraticCenter.maxTranslatedBias_quadratic_le_one line 28
5. lemma OAI.Ostmann.QuadraticCenter.quadraticBiasValue_le_one line 42
6. def OAI.Ostmann.QuadraticCenter.closedLogarithmicPrimeBand line 50
7. lemma OAI.Ostmann.QuadraticCenter.mem_closedLogarithmicPrimeBand line 54
8. lemma OAI.Ostmann.QuadraticCenter.boundedClosedLogarithmicPrimeBand_image line 66