OAI/NumberTheory/DirichletL/Detector/PrincipalEulerIdentity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.ProbeEuler.evenRatio_eq_coordR line 12
2. lemma OAI.SevenEighths.ProbeEuler.coordK_eq_geometric line 27
3. lemma OAI.SevenEighths.ProbeEuler.one_sub_ne_zero_of_norm_lt_one line 34
4. def OAI.SevenEighths.ProbeEuler.principalFullSeries line 43
5. theorem OAI.SevenEighths.ProbeEuler.principalFullSeries_euler_identity line 48
6. def OAI.SevenEighths.ProbeEuler.actualACube line 83
7. lemma OAI.SevenEighths.ProbeEuler.actualACube_sq line 86