OAI/NumberTheory/SiegelZeros/Structure/SumLogDivFilterDvdTwoMul.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.sum_log_div_filter_dvd_two_mul_le line 17
  2. theorem OAI.SiegelZeros.WeightedTorusJets.source_good_prime_mass_with_chebyshev_constant line 27
  3. theorem OAI.SiegelZeros.WeightedTorusJets.good_prime_filter_max_two line 69
  4. theorem OAI.SiegelZeros.WeightedTorusJets.good_prime_mass_extend_small_parameters line 81
  5. theorem OAI.SiegelZeros.WeightedTorusJets.source_good_prime_mass_all_parameters line 108
  6. theorem OAI.SiegelZeros.WeightedTorusJets.primitive_eighth_root_difference_pow line 131
  7. theorem OAI.SiegelZeros.WeightedTorusJets.cyclotomic_eight_sqrt_two_action line 157
  8. theorem OAI.SiegelZeros.WeightedTorusJets.chiEight_not_factorsThrough_four line 167
  9. theorem OAI.SiegelZeros.WeightedTorusJets.chiEight_isPrimitive line 178
  10. theorem OAI.SiegelZeros.WeightedTorusJets.cyclotomic_eight_adjoin_eq_characterField line 196
  11. theorem OAI.SiegelZeros.WeightedTorusJets.quadratic_character_eq_of_characterField_eq line 235
  12. theorem OAI.SiegelZeros.WeightedTorusJets.primitive_level_eq_eight_of_same_lifted_characterField line 253
  13. theorem OAI.SiegelZeros.WeightedTorusJets.primitive_level_eq_eight_of_sqrt_two_field line 274
  14. theorem OAI.SiegelZeros.WeightedTorusJets.primitive_level_eq_eight_of_lifted_sqrt_two_field line 307