OAI/NumberTheory/PrimePackets/ArtinSeries.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.GaloisIdealCharacter.artinCoefficient line 15
  2. def OAI.PrimeDegreePackets.GaloisIdealCharacter.artinDirichlet line 22
  3. def OAI.PrimeDegreePackets.GaloisIdealCharacter.badRationalPrimes line 25
  4. abbrev OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.allCoefficient line 30
  5. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.allCoefficient_bot line 32
  6. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.allCoefficient_zero line 34
  7. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.allCoefficient_one line 35
  8. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.allCoefficient_mul line 42
  9. def OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.coefficientHom line 62
  10. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.idealHom_norm line 68
  11. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.allCoefficient_norm_le_one line 74
  12. def OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.idealTerm line 81
  13. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.idealTerm_apply line 84
  14. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.idealNorm_summable line 89
  15. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.idealTerm_summable line 119
  16. def OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.normTerm line 125
  17. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.normTerm_zero line 128
  18. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.normTerm_one line 136
  19. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.normTerm_summable line 146
  20. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.normTerm_tsum line 149
  21. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.normTerm_mul line 154
  22. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.prime_idealTerm_norm_lt_one line 169
  23. theorem OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.primary_ideal_euler line 179
  24. theorem OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.local_euler line 196
  25. theorem OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.dirichlet_hasProd line 210
  26. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.local_euler_bad line 230
  27. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.ArtinSeries.local_euler_good line 259
  28. theorem OAI.PrimeDegreePackets.GaloisIdealCharacter.actual_cyclic_artin_factorization line 313