OAI/NumberTheory/Jacobsthal/Estimates/PrimitiveTransfer.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.exists_primitive_real_zero_free_disk line 11
2. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.zetaPole_real_nonneg line 62
3. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.zetaPole_real_eq line 65
4. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.exists_zeta_all_height_real_bound line 70
5. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.exists_principal_all_height_real_bound line 111
6. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.real_pole_bound_away_from_zero line 132
7. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.exists_quadratic_zero_reciprocal_bound line 168
8. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.exists_primitive_quadratic_zero_free_region line 219
9. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.exists_primitive_zero_free_region line 310
10. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.character_mod_two_eq_one line 338
11. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.primitiveCharacter_ne_one line 349
12. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.conductor_ge_three line 358
13. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.localEulerFactor_ne_zero_of_re_pos line 371
14. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.LFunction_changeLevel_ne_zero_iff line 387
15. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.LFunction_primitive_ne_zero_iff line 400