OAI/NumberTheory/Ostmann/Preliminaries/PrimeBlockResidues.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Preliminaries.allResidues line 9
2. theorem OAI.Ostmann.Preliminaries.mem_allResidues line 13
3. def OAI.Ostmann.Preliminaries.allResidueCount line 18
4. theorem OAI.Ostmann.Preliminaries.allResidueCount_eq_card line 21
5. theorem OAI.Ostmann.Preliminaries.allResidueCount_pos line 27
6. def OAI.Ostmann.Preliminaries.residueReciprocalSum line 34
7. theorem OAI.Ostmann.Preliminaries.avoids_all_neg_residues line 37
8. theorem OAI.Ostmann.Preliminaries.actual_prime_nonzero_energy_lower line 47