OAI/NumberTheory/DirichletL/Detector/PhasePowers.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.ProbePhase.residue_one_mod_four line 11
2. lemma OAI.SevenEighths.ProbePhase.odd_residue_one line 16
3. lemma OAI.SevenEighths.ProbePhase.odd_residue_pow line 20
4. lemma OAI.SevenEighths.ProbePhase.reciprocitySign_symm line 28
5. lemma OAI.SevenEighths.ProbePhase.reciprocitySign_one_left line 31
6. lemma OAI.SevenEighths.ProbePhase.reciprocitySign_mul_left line 39
7. lemma OAI.SevenEighths.ProbePhase.reciprocitySign_pow_left line 43
8. lemma OAI.SevenEighths.ProbePhase.reciprocitySign_pow_right line 50
9. lemma OAI.SevenEighths.ProbePhase.G_one line 55
10. theorem OAI.SevenEighths.ProbePhase.G_pow line 64
11. theorem OAI.SevenEighths.ProbePhase.reciprocitySign_cube_self line 74
12. theorem OAI.SevenEighths.ProbePhase.G_cube_power line 79
13. theorem OAI.SevenEighths.ProbePhase.G_completed_prime_power line 83