OAI/NumberTheory/Jacobsthal/Siegel/SqrtPairFrobeniusDirections.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Erdos970.WeightedTorusJets.sqrtPair_frobenius_directions line 17
  2. theorem OAI.Erdos970.WeightedTorusJets.mem_map_of_forall_mem_primesOver line 71
  3. theorem OAI.Erdos970.WeightedTorusJets.arithFrobAt_eq_of_under_eq line 91
  4. theorem OAI.Erdos970.WeightedTorusJets.arithFrobAt_sub_pow_mem_map line 101
  5. theorem OAI.Erdos970.WeightedTorusJets.prime_dvd_pow_sub_arithFrobAt line 119
  6. theorem OAI.Erdos970.WeightedTorusJets.ringOfIntegers_isInvariant line 136
  7. theorem OAI.Erdos970.WeightedTorusJets.exists_integer_frobenius_congruence line 147
  8. theorem OAI.Erdos970.WeightedTorusJets.cyclotomic_isUnramifiedIn line 176
  9. theorem OAI.Erdos970.WeightedTorusJets.exists_cyclotomic_frobenius_congruence line 184
  10. theorem OAI.Erdos970.WeightedTorusJets.not_isSquare_rat_two line 201
  11. theorem OAI.Erdos970.WeightedTorusJets.real_character_inv line 206
  12. theorem OAI.Erdos970.WeightedTorusJets.real_character_isQuadratic line 213
  13. theorem OAI.Erdos970.WeightedTorusJets.canonicalCyclotomicLevelNeZero line 224
  14. theorem OAI.Erdos970.WeightedTorusJets.canonicalCyclotomicExtension line 228
  15. theorem OAI.Erdos970.WeightedTorusJets.canonicalCyclotomicNumberField line 235
  16. theorem OAI.Erdos970.WeightedTorusJets.canonicalCyclotomicAbelian line 240
  17. theorem OAI.Erdos970.WeightedTorusJets.quadratic_factorsThrough_of_odd_kernel line 258
  18. theorem OAI.Erdos970.WeightedTorusJets.card_unitsMap_kernel_mul_totient line 273
  19. theorem OAI.Erdos970.WeightedTorusJets.card_unitsMap_kernel_prime_mul line 287
  20. theorem OAI.Erdos970.WeightedTorusJets.primitive_quadratic_no_odd_prime_square line 295
  21. theorem OAI.Erdos970.WeightedTorusJets.unitsMap_sixteen_mul_kernel_square line 319
  22. theorem OAI.Erdos970.WeightedTorusJets.quadratic_factorsThrough_eight_mul line 346
  23. theorem OAI.Erdos970.WeightedTorusJets.primitive_quadratic_not_sixteen_dvd line 360
  24. theorem OAI.Erdos970.WeightedTorusJets.quadratic_factorsThrough_odd_two_mul line 370
  25. theorem OAI.Erdos970.WeightedTorusJets.primitive_quadratic_mod_four_ne_two line 381
  26. theorem OAI.Erdos970.WeightedTorusJets.square_divisor_of_primitive_quadratic line 395
  27. theorem OAI.Erdos970.WeightedTorusJets.primitive_quadratic_radicand_eq_or_four_mul line 416
  28. theorem OAI.Erdos970.WeightedTorusJets.odd_divisor_primitive_quadratic_squarefree line 437
  29. theorem OAI.Erdos970.WeightedTorusJets.primitive_quadratic_conductor_shape line 448