OAI/NumberTheory/PrimePackets/FunctionalEquation.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.HeckeMellin.idealThetaXi_normalized_reflection_totallyReal line 131
  2. lemma OAI.PrimeDegreePackets.HeckeMellin.classThetaXi_reflection_totallyReal line 145
  3. theorem OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_functionalEquation_totallyReal line 172
  4. lemma OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_conj_totallyReal line 191
  5. lemma OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_one_totallyReal line 205
  6. lemma OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_zero_totallyReal line 218
  7. lemma OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_ne_zero_of_re_gt_one_totallyReal line 225
  8. lemma OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_ne_zero_of_re_neg_totallyReal line 232
  9. lemma OAI.PrimeDegreePackets.HeckeMellin.dedekindXiZeros_re_mem_Icc_totallyReal line 241
  10. lemma OAI.PrimeDegreePackets.HeckeMellin.dedekindXiZeros_ne_one_totallyReal line 251
  11. lemma OAI.PrimeDegreePackets.HeckeMellin.dedekindXiZeros_ne_zero_totallyReal line 259
  12. theorem OAI.PrimeDegreePackets.HeckeMellin.dedekindXi_hasSum_realZeroPole_totallyReal line 273
  13. lemma OAI.PrimeDegreePackets.HeckeMellin.dedekindXi_realZeroPole_nonneg_totallyReal line 289
  14. lemma OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_logDeriv_base_le_totallyReal line 303
  15. theorem OAI.PrimeDegreePackets.HeckeMellin.dedekind_near_one_zero_real_simple_unique_totallyReal line 326
  16. lemma OAI.PrimeDegreePackets.normalClosure_isTotallyReal line 356
  17. def OAI.PrimeDegreePackets.embeddingPermutation line 373
  18. lemma OAI.PrimeDegreePackets.embeddingPermutation_injective line 382
  19. theorem OAI.PrimeDegreePackets.normalClosure_finrank_le_factorial line 411
  20. theorem OAI.PrimeDegreePackets.totallyReal_normalClosure_degree line 424
  21. lemma OAI.PrimeDegreePackets.subalgebra_sup_toSubmodule_mul line 443
  22. lemma OAI.PrimeDegreePackets.intermediate_finset_sup_toSubmodule line 449
  23. theorem OAI.PrimeDegreePackets.normalClosure_integral_basis_height line 463
  24. theorem OAI.PrimeDegreePackets.normalClosure_discr_le_basis_height line 525
  25. def OAI.PrimeDegreePackets.smallIntegralBasisConstant line 543
  26. def OAI.PrimeDegreePackets.closureDiscriminantConstant line 546
  27. lemma OAI.PrimeDegreePackets.closureDiscriminantConstant_pos line 550
  28. theorem OAI.PrimeDegreePackets.normalClosure_discr_polynomial line 557
  29. theorem OAI.PrimeDegreePackets.normalClosure_log_discr_uniform line 614