OAI/NumberTheory/PrimePackets/RayEuler.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.EvenRayCharacter.allCoefficient line 16
  2. lemma OAI.PrimeDegreePackets.EvenRayCharacter.allCoefficient_bot line 23
  3. lemma OAI.PrimeDegreePackets.EvenRayCharacter.allCoefficient_zero line 26
  4. lemma OAI.PrimeDegreePackets.EvenRayCharacter.allCoefficient_one line 28
  5. lemma OAI.PrimeDegreePackets.EvenRayCharacter.integralUnit_mul line 35
  6. lemma OAI.PrimeDegreePackets.EvenRayCharacter.allCoefficient_mul line 41
  7. def OAI.PrimeDegreePackets.EvenRayCharacter.coefficientHom line 63
  8. lemma OAI.PrimeDegreePackets.EvenRayCharacter.allCoefficient_norm_le_one line 69
  9. lemma OAI.PrimeDegreePackets.EvenRayCharacter.allCoefficient_underlying line 77
  10. lemma OAI.PrimeDegreePackets.EvenRayCharacter.norm_underlying line 82
  11. def OAI.PrimeDegreePackets.EvenRayCharacter.idealTerm line 87
  12. lemma OAI.PrimeDegreePackets.EvenRayCharacter.idealTerm_apply line 91
  13. lemma OAI.PrimeDegreePackets.EvenRayCharacter.idealTerm_underlying line 94
  14. lemma OAI.PrimeDegreePackets.EvenRayCharacter.idealTerm_summable_nonzero line 100
  15. lemma OAI.PrimeDegreePackets.EvenRayCharacter.idealTerm_summable line 112
  16. lemma OAI.PrimeDegreePackets.EvenRayCharacter.dirichlet_eq_ideal_tsum line 121
  17. def OAI.PrimeDegreePackets.EvenRayCharacter.normTerm line 138
  18. lemma OAI.PrimeDegreePackets.EvenRayCharacter.normTerm_zero line 141
  19. lemma OAI.PrimeDegreePackets.EvenRayCharacter.normTerm_one line 149
  20. lemma OAI.PrimeDegreePackets.EvenRayCharacter.normTerm_summable line 159
  21. lemma OAI.PrimeDegreePackets.EvenRayCharacter.normTerm_tsum line 162
  22. lemma OAI.PrimeDegreePackets.EvenRayCharacter.normTerm_mul line 167
  23. lemma OAI.PrimeDegreePackets.EvenRayCharacter.prime_idealTerm_norm_lt_one line 182
  24. theorem OAI.PrimeDegreePackets.EvenRayCharacter.primary_ideal_euler line 192
  25. theorem OAI.PrimeDegreePackets.EvenRayCharacter.local_euler line 209
  26. theorem OAI.PrimeDegreePackets.EvenRayCharacter.dirichlet_hasProd line 223
  27. theorem OAI.PrimeDegreePackets.EvenRayCharacter.dirichlet_ne_zero line 238
  28. theorem OAI.PrimeDegreePackets.EvenRayCharacter.continued_ne_zero_of_one_lt_re line 254