OAI/NumberTheory/PrimePackets/CosetMeromorphic.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.GaloisIdealCharacter.rationalPrimeSpectrum line 16
  2. def OAI.PrimeDegreePackets.GaloisIdealCharacter.cosetRationalEuler line 26
  3. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.cosetRationalEuler_good line 34
  4. def OAI.PrimeDegreePackets.GaloisIdealCharacter.removedEulerPolynomial line 67
  5. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.primeEuler_denominator_ne_zero line 71
  6. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.removedEulerPolynomial_entire line 81
  7. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.removedEulerPolynomial_ne_zero line 92
  8. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.cosetRationalEuler_hasProd line 102
  9. def OAI.PrimeDegreePackets.GaloisIdealCharacter.cosetMeromorphic line 134
  10. def OAI.PrimeDegreePackets.GaloisIdealCharacter.cosetXiFactor line 138
  11. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.gammaInverse_entire line 143
  12. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.exponentialInverse_entire line 149
  13. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.cosetXiFactor_meromorphicAt line 156
  14. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.cosetXiFactor_analyticAt line 165
  15. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.cosetXiFactor_ne_zero line 174
  16. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.cosetMeromorphic_eq_factor line 183
  17. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.cosetMeromorphic_meromorphicAt line 191
  18. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.cosetMeromorphic_eq_dedekindZeta line 197
  19. theorem OAI.PrimeDegreePackets.GaloisIdealCharacter.cosetMeromorphic_order_eq line 209
  20. theorem OAI.PrimeDegreePackets.GaloisIdealCharacter.actual_coset_meromorphic_pairing line 223