OAI/NumberTheory/SiegelZeros/Determinants/ThetaDivisibility.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.Awei.W39.theta line 22
  2. theorem OAI.SiegelZeros.Awei.W39.legendre_cast_eq_pow line 28
  3. theorem OAI.SiegelZeros.Awei.W39.root_pow_prime line 33
  4. theorem OAI.SiegelZeros.Awei.W39.intCast_pow_prime line 44
  5. theorem OAI.SiegelZeros.Awei.W39.theta_pow_prime line 47
  6. theorem OAI.SiegelZeros.Awei.W39.theta_pow_prime_negative line 54
  7. theorem OAI.SiegelZeros.Awei.W39.theta_frobenius_dvd line 62
  8. theorem OAI.SiegelZeros.Awei.W39.legendre_two_sign line 83
  9. theorem OAI.SiegelZeros.Awei.W39.theta_frobenius_two_conjugates line 91
  10. theorem OAI.SiegelZeros.SiegelZerosAwei.W41.det_lower_unitriangular_mul line 119
  11. theorem OAI.SiegelZeros.SiegelZerosAwei.W41.exists_lower_unitriangular_of_row_sub_mem_span line 129
  12. theorem OAI.SiegelZeros.SiegelZerosAwei.W41.det_eq_of_row_sub_mem_span line 159
  13. theorem OAI.SiegelZeros.SiegelZerosAwei.W41.det_eq_in_integral_ring_of_ambient_row_span line 167
  14. def OAI.SiegelZeros.WeightedTorusJets.W42.replacementEntry line 187
  15. theorem OAI.SiegelZeros.WeightedTorusJets.W42.pow_dvd_replacementEntry line 190
  16. theorem OAI.SiegelZeros.WeightedTorusJets.W42.replacementEntry_mem_principal line 196
  17. theorem OAI.SiegelZeros.WeightedTorusJets.W42.prod_dvd_det_of_row_dvd line 205
  18. theorem OAI.SiegelZeros.WeightedTorusJets.W42.pow_sum_dvd_det_of_row_dvd line 216
  19. theorem OAI.SiegelZeros.WeightedTorusJets.W42.pow_sum_dvd_replacement_det line 222
  20. theorem OAI.SiegelZeros.WeightedTorusJets.W42.floor_sum_dvd_replacement_det line 233
  21. theorem OAI.SiegelZeros.WeightedTorusJets.W42.det_eq_of_map_det_eq line 242
  22. theorem OAI.SiegelZeros.WeightedTorusJets.W42.pow_sum_dvd_det_of_map_det_eq line 248
  23. theorem OAI.SiegelZeros.WeightedTorusJets.W43.integral_norm_cast line 268
  24. theorem OAI.SiegelZeros.WeightedTorusJets.W43.integral_norm_natCast line 272
  25. theorem OAI.SiegelZeros.WeightedTorusJets.W43.norm_dvd_of_scalar_pow_dvd line 278
  26. theorem OAI.SiegelZeros.WeightedTorusJets.W43.quartic_norm_dvd line 285
  27. theorem OAI.SiegelZeros.WeightedTorusJets.W43.quartic_norm_dvd_of_mem line 290
  28. theorem OAI.SiegelZeros.WeightedTorusJets.W43.prime_product_dvd_norm line 296
  29. theorem OAI.SiegelZeros.WeightedTorusJets.W43.integral_norm_ne_zero line 307
  30. theorem OAI.SiegelZeros.WeightedTorusJets.W45.prime_power_product_dvd line 318
  31. theorem OAI.SiegelZeros.WeightedTorusJets.W45.weighted_prime_log_le line 327
  32. theorem OAI.SiegelZeros.WeightedTorusJets.W45.weighted_prime_log_le_div_degree line 352
  33. theorem OAI.SiegelZeros.WeightedTorusJets.W45.quartic_weighted_prime_log_le line 360
  34. theorem OAI.SiegelZeros.WeightedTorusJets.W45.quartic_integral_norm_log_lower line 379
  35. def OAI.SiegelZeros.SiegelZerosAwei.W60.rows line 406
  36. def OAI.SiegelZeros.SiegelZerosAwei.W60.EarlierSpan line 409
  37. theorem OAI.SiegelZeros.SiegelZerosAwei.W60.determinant_dvd_second line 415
  38. theorem OAI.SiegelZeros.SiegelZerosAwei.W60.EarlierSpan.swap line 450
  39. theorem OAI.SiegelZeros.SiegelZerosAwei.W60.determinant_dvd_either line 462
  40. theorem OAI.SiegelZeros.SiegelZerosAwei.W60.theta_determinant_dvd line 477
  41. theorem OAI.SiegelZeros.SiegelZerosAwei.W60.theta_integer_norm_dvd line 495