OAI/NumberTheory/SiegelZeros/Determinants/GeneratedGreedyDivisibility.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.SiegelZerosAwei.W37.thetaIntegral line 20
  2. def OAI.SiegelZeros.SiegelZerosAwei.W37.thetaField line 23
  3. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.coe_thetaIntegral line 26
  4. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.thetaField_isIntegral line 30
  5. def OAI.SiegelZeros.SiegelZerosAwei.W37.rowIntegral line 35
  6. def OAI.SiegelZeros.SiegelZerosAwei.W37.rowField line 41
  7. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.coe_rowIntegral line 46
  8. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.rowField_isIntegral line 55
  9. def OAI.SiegelZeros.SiegelZerosAwei.W37.deltaIntegral line 63
  10. def OAI.SiegelZeros.SiegelZerosAwei.W37.deltaField line 67
  11. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.coe_deltaIntegral line 71
  12. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.deltaField_isIntegral line 80
  13. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.norm_nonzero_integer line 88
  14. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.delta_norm_nonzero_integer line 96
  15. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.integer_norm_natCast line 105
  16. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.norm_dvd_of_pow_dvd line 115
  17. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.norm_dvd_of_pow_dvd_degree_four line 122
  18. def OAI.SiegelZeros.SiegelZerosAwei.W37.automorphismDirections line 139
  19. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.coe_rowIntegral_eq_derivativeMatrix line 143
  20. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.coe_deltaIntegral_eq_derivativeMatrix_det line 154
  21. def OAI.SiegelZeros.SiegelZerosAwei.W37.adjoinIntegralGenerators line 170
  22. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.coe_adjoinIntegralGenerators line 177
  23. def OAI.SiegelZeros.SiegelZerosAwei.W37.actualSigma line 182
  24. def OAI.SiegelZeros.SiegelZerosAwei.W37.actualSigmaTau line 188
  25. def OAI.SiegelZeros.SiegelZerosAwei.W37.concreteDirections line 194
  26. def OAI.SiegelZeros.SiegelZerosAwei.W37.concreteDelta line 201
  27. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.coe_concreteDelta line 210
  28. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.concreteDelta_ne_zero line 220
  29. def OAI.SiegelZeros.SiegelZerosAwei.W37.integralRootA line 242
  30. def OAI.SiegelZeros.SiegelZerosAwei.W37.integralRootB line 246
  31. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.integralRootA_sq line 251
  32. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.integralRootB_sq line 260
  33. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.adjoinIntegralGenerators_eq line 269
  34. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.thetaIntegral_eq_coordinateTheta line 278
  35. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.integralSigma_rootA line 288
  36. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.integralSigma_rootB line 299
  37. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.integralSigmaTau_rootA line 310
  38. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.integralSigmaTau_rootB line 321
  39. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.rowIntegral_eq_coordinateRow line 332
  40. theorem OAI.SiegelZeros.SiegelZerosAwei.W37.concreteDelta_eq_coordinateRows_det line 350
  41. def OAI.SiegelZeros.SiegelZerosAwei.W60.weightedRow line 381
  42. def OAI.SiegelZeros.SiegelZerosAwei.W60.greedySet line 385
  43. def OAI.SiegelZeros.SiegelZerosAwei.W60.greedyIndex line 389
  44. theorem OAI.SiegelZeros.SiegelZerosAwei.W60.greedy_card_of_spanning line 394
  45. theorem OAI.SiegelZeros.SiegelZerosAwei.W60.greedy_earlierSpan line 402
  46. theorem OAI.SiegelZeros.SiegelZerosAwei.W60.greedy_det_ne_zero line 435
  47. theorem OAI.SiegelZeros.SiegelZerosAwei.W60.greedy_determinant_dvd line 467
  48. theorem OAI.SiegelZeros.SiegelZerosAwei.W60.greedy_theta_determinant_dvd line 480
  49. theorem OAI.SiegelZeros.SiegelZerosAwei.W60.exists_greedy_theta_divisibility line 502
  50. def OAI.SiegelZeros.SiegelZerosAwei.W60.generatedRootA line 544
  51. def OAI.SiegelZeros.SiegelZerosAwei.W60.generatedRootB line 547
  52. theorem OAI.SiegelZeros.SiegelZerosAwei.W60.generatedRootA_sq line 551
  53. theorem OAI.SiegelZeros.SiegelZerosAwei.W60.generatedRootB_sq line 556
  54. theorem OAI.SiegelZeros.SiegelZerosAwei.W60.exists_generated_greedy_divisibility line 561
  55. theorem OAI.SiegelZeros.SiegelZerosAwei.W60.exists_concrete_greedy_divisibility line 592