OAI/NumberTheory/SiegelZeros/Determinants/SqrtPairFrobeniusDirections.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SiegelZeros.WeightedTorusJets.sqrtPair_frobenius_directions line 15
  2. theorem OAI.SiegelZeros.WeightedTorusJets.mem_map_of_forall_mem_primesOver line 65
  3. theorem OAI.SiegelZeros.WeightedTorusJets.arithFrobAt_eq_of_under_eq line 85
  4. theorem OAI.SiegelZeros.WeightedTorusJets.arithFrobAt_sub_pow_mem_map line 95
  5. theorem OAI.SiegelZeros.WeightedTorusJets.prime_dvd_pow_sub_arithFrobAt line 113
  6. theorem OAI.SiegelZeros.WeightedTorusJets.ringOfIntegers_isInvariant line 130
  7. theorem OAI.SiegelZeros.WeightedTorusJets.exists_integer_frobenius_congruence line 141
  8. theorem OAI.SiegelZeros.WeightedTorusJets.cyclotomic_isUnramifiedIn line 168
  9. theorem OAI.SiegelZeros.WeightedTorusJets.exists_cyclotomic_frobenius_congruence line 176
  10. theorem OAI.SiegelZeros.WeightedTorusJets.not_isSquare_rat_two line 191
  11. theorem OAI.SiegelZeros.WeightedTorusJets.real_character_inv line 194
  12. theorem OAI.SiegelZeros.WeightedTorusJets.real_character_isQuadratic line 201
  13. theorem OAI.SiegelZeros.WeightedTorusJets.canonicalCyclotomicLevelNeZero line 210
  14. theorem OAI.SiegelZeros.WeightedTorusJets.canonicalCyclotomicExtension line 214
  15. theorem OAI.SiegelZeros.WeightedTorusJets.canonicalCyclotomicNumberField line 221
  16. theorem OAI.SiegelZeros.WeightedTorusJets.canonicalCyclotomicAbelian line 226
  17. theorem OAI.SiegelZeros.WeightedTorusJets.quadratic_factorsThrough_of_odd_kernel line 234
  18. theorem OAI.SiegelZeros.WeightedTorusJets.card_unitsMap_kernel_mul_totient line 249
  19. theorem OAI.SiegelZeros.WeightedTorusJets.card_unitsMap_kernel_prime_mul line 263
  20. theorem OAI.SiegelZeros.WeightedTorusJets.primitive_quadratic_no_odd_prime_square line 271
  21. theorem OAI.SiegelZeros.WeightedTorusJets.unitsMap_sixteen_mul_kernel_square line 295
  22. theorem OAI.SiegelZeros.WeightedTorusJets.quadratic_factorsThrough_eight_mul line 322
  23. theorem OAI.SiegelZeros.WeightedTorusJets.primitive_quadratic_not_sixteen_dvd line 336
  24. theorem OAI.SiegelZeros.WeightedTorusJets.quadratic_factorsThrough_odd_two_mul line 346
  25. theorem OAI.SiegelZeros.WeightedTorusJets.primitive_quadratic_mod_four_ne_two line 357
  26. theorem OAI.SiegelZeros.WeightedTorusJets.square_divisor_of_primitive_quadratic line 371
  27. theorem OAI.SiegelZeros.WeightedTorusJets.primitive_quadratic_radicand_eq_or_four_mul line 392
  28. theorem OAI.SiegelZeros.WeightedTorusJets.odd_divisor_primitive_quadratic_squarefree line 413
  29. theorem OAI.SiegelZeros.WeightedTorusJets.primitive_quadratic_conductor_shape line 424