OAI/NumberTheory/Jacobsthal/Sieve/ResidueProjection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.ErdosVarianceMoments.cast_nat_residue line 13
2. theorem OAI.Erdos970.ErdosVarianceMoments.int_isCoprime_of_natAbs line 19
3. def OAI.Erdos970.ErdosVarianceMoments.divisorPhase line 23
4. def OAI.Erdos970.ErdosVarianceMoments.patternPValue line 25
5. def OAI.Erdos970.ErdosVarianceMoments.patternKValue line 27
6. def OAI.Erdos970.ErdosVarianceMoments.divisorPhaseUnit line 30
7. theorem OAI.Erdos970.ErdosVarianceMoments.divisorPhaseUnit_coe line 39
8. theorem OAI.Erdos970.ErdosVarianceMoments.prime_divisorPhase_eq line 43
9. theorem OAI.Erdos970.ErdosVarianceMoments.primePoint_pValue line 55
10. theorem OAI.Erdos970.ErdosVarianceMoments.primePoint_kValue line 61