OAI/NumberTheory/DirichletL/Arithmetic/EisensteinIdeals.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ActualEisensteinSieve.K line 17
  2. abbrev OAI.ActualEisensteinSieve.O line 18
  3. instance OAI.ActualEisensteinSieve.(instance at line 20) line 20
  4. instance OAI.ActualEisensteinSieve.(instance at line 23) line 23
  5. def OAI.ActualEisensteinSieve.omega line 26
  6. def OAI.ActualEisensteinSieve.lambda line 29
  7. def OAI.ActualEisensteinSieve.lambdaIdeal line 31
  8. theorem OAI.ActualEisensteinSieve.lambda_prime line 33
  9. theorem OAI.ActualEisensteinSieve.lambda_maximal line 37
  10. theorem OAI.ActualEisensteinSieve.lambda_card line 44
  11. example OAI.ActualEisensteinSieve.(example at line 52) line 52
  12. example OAI.ActualEisensteinSieve.(example at line 53) line 53
  13. def OAI.ActualEisensteinSieve.localQuadratic line 55
  14. theorem OAI.ActualEisensteinSieve.localQuadratic_one line 61
  15. theorem OAI.ActualEisensteinSieve.localQuadratic_mul line 69
  16. theorem OAI.ActualEisensteinSieve.localQuadratic_zero_iff line 73
  17. theorem OAI.ActualEisensteinSieve.exists_localQuadratic_neg_one line 82
  18. theorem OAI.ActualEisensteinSieve.localQuadratic_neg_one line 94
  19. theorem OAI.ActualEisensteinSieve.localQuadratic_cube_root_one line 103
  20. theorem OAI.ActualEisensteinSieve.localQuadratic_trichotomy line 124
  21. instance OAI.ActualEisensteinSieve.(instance at line 136) line 136
  22. theorem OAI.ActualEisensteinSieve.lambda_residue_odd line 138
  23. theorem OAI.ActualEisensteinSieve.lambdaQuadratic_neg_one line 147
  24. theorem OAI.ActualEisensteinSieve.finite_prod_trichotomy line 151
  25. theorem OAI.ActualEisensteinSieve.crt_pair line 172
  26. theorem OAI.ActualEisensteinSieve.localQuadratic_congr line 183
  27. theorem OAI.ActualEisensteinSieve.lambdaQuadratic_omega line 188
  28. theorem OAI.ActualEisensteinSieve.productQuadratic_detects_left line 194
  29. theorem OAI.ActualEisensteinSieve.productQuadratic_not_factor_right line 208
  30. theorem OAI.ActualEisensteinSieve.productQuadratic_not_factor_left line 227
  31. theorem OAI.ActualEisensteinSieve.finiteQuadratic_detects_prime line 240
  32. def OAI.ActualEisensteinSieve.quadraticProduct line 270
  33. theorem OAI.ActualEisensteinSieve.quadraticProduct_one line 275
  34. theorem OAI.ActualEisensteinSieve.quadraticProduct_mul line 280
  35. theorem OAI.ActualEisensteinSieve.quadraticProduct_neg_one_square line 286
  36. def OAI.ActualEisensteinSieve.correctedQuadraticProduct line 295
  37. theorem OAI.ActualEisensteinSieve.correctedQuadraticProduct_neg_one line 301
  38. theorem OAI.ActualEisensteinSieve.correctedQuadraticProduct_omega line 314
  39. theorem OAI.ActualEisensteinSieve.correctedQuadraticProduct_one line 326
  40. theorem OAI.ActualEisensteinSieve.correctedQuadraticProduct_mul line 335
  41. def OAI.ActualEisensteinSieve.correctedQuadraticHom line 346
  42. theorem OAI.ActualEisensteinSieve.correctedQuadraticProduct_units line 353
  43. theorem OAI.ActualEisensteinSieve.correctedQuadraticProduct_congr_mod_conductor line 394
  44. theorem OAI.ActualEisensteinSieve.correctedQuadraticProduct_one_of_congruent line 417
  45. def OAI.ActualEisensteinSieve.correctedAssociatesHom line 428
  46. def OAI.ActualEisensteinSieve.idealGeneratorClass line 447
  47. theorem OAI.ActualEisensteinSieve.idealGeneratorClass_one line 451
  48. theorem OAI.ActualEisensteinSieve.idealGeneratorClass_mul line 455
  49. theorem OAI.ActualEisensteinSieve.idealGeneratorClass_span line 462
  50. def OAI.ActualEisensteinSieve.correctedIdealHom line 469
  51. theorem OAI.ActualEisensteinSieve.correctedIdealHom_span line 479
  52. theorem OAI.ActualEisensteinSieve.finiteQuadratic_not_factor_without_prime line 487
  53. theorem OAI.ActualEisensteinSieve.finiteQuadratic_not_factor_omit_prime_ideal line 512
  54. theorem OAI.ActualEisensteinSieve.finiteQuadratic_congr_mod_product line 552
  55. def OAI.ActualEisensteinSieve.finiteQuadraticOnQuotient line 567
  56. theorem OAI.ActualEisensteinSieve.finiteQuadraticOnQuotient_mk line 573
  57. theorem OAI.ActualEisensteinSieve.finiteQuadratic_not_factor_subproduct line 584
  58. def OAI.ActualEisensteinSieve.squarefreeCRT line 629
  59. theorem OAI.ActualEisensteinSieve.squarefreeCRT_mk line 643
  60. def OAI.ActualEisensteinSieve.localResidueChar line 655
  61. theorem OAI.ActualEisensteinSieve.localResidueChar_zero_iff line 662
  62. def OAI.ActualEisensteinSieve.squarefreePiChar line 670
  63. def OAI.ActualEisensteinSieve.squarefreeQuotientChar line 695
  64. theorem OAI.ActualEisensteinSieve.squarefreeQuotientChar_mk line 714
  65. theorem OAI.ActualEisensteinSieve.squarefreeQuotientChar_primitive line 728
  66. theorem OAI.ActualEisensteinSieve.squarefreeQuotientChar_isQuadratic line 746
  67. theorem OAI.ActualEisensteinSieve.squarefreeQuotientChar_order_two line 759
  68. theorem OAI.ActualEisensteinSieve.correctedQuadraticProduct_not_factor_without_lambda line 766
  69. theorem OAI.ActualEisensteinSieve.lambdaQuadratic_sq_one_of_not_mem line 802
  70. theorem OAI.ActualEisensteinSieve.correctedQuadraticProduct_pair_cancel line 810
  71. theorem OAI.ActualEisensteinSieve.correctedQuadraticProduct_not_factor_without_prime line 834