OAI/NumberTheory/DirichletL/Reciprocity/CubicJacobi.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CubicJacobiGlobal.O line 75
  2. abbrev OAI.CubicJacobiGlobal.K line 76
  3. def OAI.CubicJacobiGlobal.primeValue line 79
  4. theorem OAI.CubicJacobiGlobal.primeValue_eq line 85
  5. def OAI.CubicJacobiGlobal.idealSymbol line 91
  6. theorem OAI.CubicJacobiGlobal.idealSymbol_zero line 95
  7. theorem OAI.CubicJacobiGlobal.idealSymbol_bot line 96
  8. theorem OAI.CubicJacobiGlobal.idealSymbol_one line 97
  9. theorem OAI.CubicJacobiGlobal.idealSymbol_top line 100
  10. theorem OAI.CubicJacobiGlobal.idealSymbol_mul line 103
  11. def OAI.CubicJacobiGlobal.symbol line 114
  12. theorem OAI.CubicJacobiGlobal.symbol_one line 116
  13. theorem OAI.CubicJacobiGlobal.symbol_zero line 117
  14. theorem OAI.CubicJacobiGlobal.symbol_mul_denominator line 119
  15. theorem OAI.CubicJacobiGlobal.idealSymbol_prime line 124
  16. theorem OAI.CubicJacobiGlobal.factor_good line 132
  17. theorem OAI.CubicJacobiGlobal.idealSymbol_map_mul line 138
  18. theorem OAI.CubicJacobiGlobal.idealSymbol_map_one line 150
  19. theorem OAI.CubicJacobiGlobal.idealSymbol_map_multiset_prod line 161
  20. theorem OAI.CubicJacobiGlobal.symbol_prime line 168
  21. theorem OAI.CubicJacobiGlobal.idealSymbol_reciprocity line 176
  22. theorem OAI.CubicJacobiGlobal.symbol_reciprocity line 202
  23. theorem OAI.CubicJacobiGlobal.idealSymbol_congr line 211
  24. theorem OAI.CubicJacobiGlobal.symbol_congr line 227
  25. abbrev OAI.CubicRamified.O line 235
  26. abbrev OAI.CubicRamified.K line 236
  27. lemma OAI.CubicRamified.lambda_def line 239
  28. theorem OAI.CubicRamified.cubicValue_cube line 241
  29. theorem OAI.CubicRamified.cubicValue_ne_zero line 248
  30. theorem OAI.CubicRamified.ramified_comparison line 256
  31. def OAI.CubicRamified.sevenPrime line 301
  32. def OAI.CubicRamified.sevenIdeal line 302
  33. theorem OAI.CubicRamified.sevenPrime_norm line 304
  34. theorem OAI.CubicRamified.sevenPrime_ne_zero line 310
  35. theorem OAI.CubicRamified.sevenIdeal_norm line 319
  36. instance OAI.CubicRamified.sevenIdeal_isMaximal line 322
  37. theorem OAI.CubicRamified.sevenPrime_primary line 328
  38. theorem OAI.CubicRamified.sevenIdeal_good line 334
  39. theorem OAI.CubicRamified.twoIdeal_card line 338
  40. theorem OAI.CubicRamified.sevenIdeal_card line 347
  41. theorem OAI.CubicRamified.cubicValue_lambda_two line 349
  42. theorem OAI.CubicRamified.cubicValue_lambda_seven line 362
  43. def OAI.CubicRamified.primaryCoord line 378
  44. theorem OAI.CubicRamified.primaryCoord_eq line 380
  45. theorem OAI.CubicRamified.primaryCoord_primary line 386
  46. theorem OAI.CubicRamified.primaryCoord_ne_zero line 391
  47. lemma OAI.CubicRamified.primary_card_exponent line 399
  48. theorem OAI.CubicRamified.cubicValue_omega_primary line 412
  49. theorem OAI.CubicRamified.ramified_comparison_of_factor line 435
  50. lemma OAI.CubicRamified.omega_ne_zero line 459
  51. lemma OAI.CubicRamified.omega_isUnit line 460
  52. lemma OAI.CubicRamified.omega_four line 461
  53. lemma OAI.CubicRamified.omega_five line 465
  54. lemma OAI.CubicRamified.cubicValue_neg line 470
  55. lemma OAI.CubicRamified.cubicValue_omega_two line 475
  56. lemma OAI.CubicRamified.cubicValue_omega_seven line 478
  57. lemma OAI.CubicRamified.eq_of_cube_one_of_sq_eq line 482
  58. lemma OAI.CubicRamified.supplement_of_factor line 491
  59. lemma OAI.CubicRamified.omega_six line 510
  60. lemma OAI.CubicRamified.omega_seven line 515
  61. lemma OAI.CubicRamified.omega_eight line 520
  62. theorem OAI.CubicRamified.supplement_case00 line 525
  63. theorem OAI.CubicRamified.supplement_case01 line 548
  64. theorem OAI.CubicRamified.supplement_case02 line 571
  65. theorem OAI.CubicRamified.supplement_case10 line 591
  66. theorem OAI.CubicRamified.supplement_case11 line 612
  67. theorem OAI.CubicRamified.supplement_case12 line 633
  68. theorem OAI.CubicRamified.supplement_case20 line 656
  69. theorem OAI.CubicRamified.supplement_case21 line 679
  70. theorem OAI.CubicRamified.supplement_case22 line 699
  71. theorem OAI.CubicRamified.cubicValue_lambda_primary line 719