OAI/NumberTheory/PrimePackets/NormalClosure.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.isTotallyReal_of_isNormalClosure line 133
  2. lemma OAI.PrimeDegreePackets.abs_discr_le_of_algHom line 143
  3. lemma OAI.PrimeDegreePackets.normalClosure_abs_discr_ge line 154
  4. lemma OAI.PrimeDegreePackets.HeckeMellin.boundedDegree_near_one_zero_real_simple_unique line 167
  5. theorem OAI.PrimeDegreePackets.HeckeMellin.normalClosure_zero_box_uniform line 190
  6. lemma OAI.PrimeDegreePackets.HeckeMellin.integralFractionalIdeals_norm_summable line 237
  7. lemma OAI.PrimeDegreePackets.HeckeMellin.integralFractionalIdeals_absNorm_ge_one line 246
  8. def OAI.PrimeDegreePackets.HeckeMellin.idealClassDirichlet line 255
  9. lemma OAI.PrimeDegreePackets.HeckeMellin.idealClassDirichlet_summable line 260
  10. lemma OAI.PrimeDegreePackets.HeckeMellin.idealClassDirichlet_differentiableOn line 272
  11. def OAI.PrimeDegreePackets.HeckeMellin.idealClassThetaXi line 298
  12. lemma OAI.PrimeDegreePackets.HeckeMellin.idealClassThetaXi_entire line 305
  13. lemma OAI.PrimeDegreePackets.HeckeMellin.idealClassDirichlet_partition line 317
  14. lemma OAI.PrimeDegreePackets.HeckeMellin.idealThetaMellin_normalized_real line 339
  15. theorem OAI.PrimeDegreePackets.HeckeMellin.idealClassThetaXi_real_eq line 366
  16. def OAI.PrimeDegreePackets.HeckeMellin.completedIdealClassXi line 402
  17. lemma OAI.PrimeDegreePackets.HeckeMellin.completedIdealClassXi_entire line 409
  18. lemma OAI.PrimeDegreePackets.HeckeMellin.completedIdealClassXi_real_eq line 416
  19. theorem OAI.PrimeDegreePackets.HeckeMellin.completedIdealClassXi_eq line 442
  20. lemma OAI.PrimeDegreePackets.HeckeMellin.idealThetaXi_zero_value line 459
  21. lemma OAI.PrimeDegreePackets.HeckeMellin.idealThetaXi_normalized_one_value line 466
  22. lemma OAI.PrimeDegreePackets.HeckeMellin.idealClassThetaXi_zero_of_sum_eq_zero line 478
  23. lemma OAI.PrimeDegreePackets.HeckeMellin.idealClassThetaXi_one_of_sum_eq_zero line 488
  24. lemma OAI.PrimeDegreePackets.HeckeMellin.finite_group_character_sum_eq_zero line 503
  25. def OAI.PrimeDegreePackets.HeckeMellin.entireIdealClassL line 518
  26. lemma OAI.PrimeDegreePackets.HeckeMellin.entire_dslope line 523
  27. lemma OAI.PrimeDegreePackets.HeckeMellin.entireIdealClassL_entire line 528
  28. lemma OAI.PrimeDegreePackets.HeckeMellin.completedIdealClassXi_zero_of_sum_eq_zero line 534
  29. lemma OAI.PrimeDegreePackets.HeckeMellin.completedIdealClassXi_one_of_sum_eq_zero line 541
  30. theorem OAI.PrimeDegreePackets.HeckeMellin.entireIdealClassL_eq line 550
  31. theorem OAI.PrimeDegreePackets.HeckeMellin.nonprincipalHeckeL_entire_and_eq line 571