OAI/NumberTheory/SiegelZeros/Characters/CharacterMaster.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.W07.quadratic_of_real line 16
  2. def OAI.SiegelZeros.W07.primeWeight line 31
  3. def OAI.SiegelZeros.W07.primeMass line 33
  4. def OAI.SiegelZeros.W07.valuePrimes line 35
  5. def OAI.SiegelZeros.W07.goodPrimes line 40
  6. def OAI.SiegelZeros.W07.discardedNegativePrimes line 45
  7. theorem OAI.SiegelZeros.W07.prime_mass_partition line 50
  8. theorem OAI.SiegelZeros.W07.negative_mass_partition line 61
  9. theorem OAI.SiegelZeros.W07.good_mass_lower_bound line 72
  10. theorem OAI.SiegelZeros.W07.negative_prime_not_dvd line 86
  11. theorem OAI.SiegelZeros.W07.negative_large_prime_not_dvd_two_mul line 94
  12. theorem OAI.SiegelZeros.W07.prime_value_zero_iff_dvd line 103
  13. theorem OAI.SiegelZeros.W07.discarded_eq_small_negative line 114
  14. theorem OAI.SiegelZeros.SiegelZerosAwei.W46.order_image_card line 144
  15. theorem OAI.SiegelZeros.SiegelZerosAwei.W46.order_image_sum line 151
  16. theorem OAI.SiegelZeros.SiegelZerosAwei.W46.concrete_master_of_norm_divisibility line 157
  17. theorem OAI.SiegelZeros.SiegelZerosAwei.W50.actual_character_selection line 270
  18. theorem OAI.SiegelZeros.SiegelZerosAwei.W50.actual_character_orders line 314
  19. theorem OAI.SiegelZeros.SiegelZerosAwei.W50.exists_actual_character_pivot_master line 354