OAI/NumberTheory/Jacobsthal/Primes/PrincipalPrimePowers.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.principalDifference line 14
2. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.principalDifference_norm_le line 18
3. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.excluded_primePower_dvd_power line 27
4. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.principalDifference_eq_zero_of_not_dvd line 42
5. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.norm_principal_sharp_difference line 50
6. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.natLog_floor_le_realLog line 80
7. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.norm_principal_sharp_difference_real line 96