OAI/NumberTheory/Jacobsthal/Sieve/PrimeFibreBrunBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.ErdosPrimeInputs.BrunTitchmarshUpper.finite_prime_set_upper line 15
2. def OAI.Erdos970.ErdosPrimeInputs.BrunTitchmarshUpper.intervalPrimes line 56
3. theorem OAI.Erdos970.ErdosPrimeInputs.BrunTitchmarshUpper.mem_intervalPrimes line 60
4. theorem OAI.Erdos970.ErdosPrimeInputs.BrunTitchmarshUpper.brun_titchmarsh_upper line 71
5. def OAI.Erdos970.ErdosVarianceSmallModel.residueFibre line 87
6. theorem OAI.Erdos970.ErdosVarianceSmallModel.residue_fibre_prime_bound line 90