OAI/NumberTheory/DirichletL/Detector/EulerCoordinates.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.ProbeEuler.coordV line 11
  2. def OAI.SevenEighths.ProbeEuler.coordR line 12
  3. def OAI.SevenEighths.ProbeEuler.coordW line 13
  4. def OAI.SevenEighths.ProbeEuler.coordD line 14
  5. def OAI.SevenEighths.ProbeEuler.coordK line 15
  6. def OAI.SevenEighths.ProbeEuler.unramifiedClosed line 17
  7. def OAI.SevenEighths.ProbeEuler.actualAPhase line 25
  8. def OAI.SevenEighths.ProbeEuler.actualUnramifiedClosed line 28
  9. lemma OAI.SevenEighths.ProbeEuler.actualAPhase_norm_le_one line 35
  10. lemma OAI.SevenEighths.ProbeEuler.coordV_norm line 42
  11. lemma OAI.SevenEighths.ProbeEuler.coordR_norm_le line 47
  12. lemma OAI.SevenEighths.ProbeEuler.coordW_norm_le line 54
  13. lemma OAI.SevenEighths.ProbeEuler.coordD_norm_le line 59
  14. lemma OAI.SevenEighths.ProbeEuler.coordK_norm_le line 67