OAI/NumberTheory/DirichletL/GaussSum/RayCharacters.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RayFourExpansion.prime_unit_mod_four line 78
  2. theorem OAI.RayFourExpansion.prime_product_unit_mod_four line 110
  3. theorem OAI.RayFourExpansion.rayMask_prime_product line 117
  4. theorem OAI.RayFourExpansion.canonicalProductG_character_expansion line 123
  5. theorem OAI.RayFourExpansion.quadraticCrossPhase_character_expansion line 137
  6. theorem OAI.MixedCrossSeparation.converted_active_row_observations line 159
  7. theorem OAI.MixedCrossSeparation.convertedColumnBlock_image line 199
  8. theorem OAI.MixedCrossSeparation.quadraticCrossPhase_image line 213
  9. theorem OAI.MixedCrossSeparation.negative_active_image line 227
  10. theorem OAI.MixedCrossSeparation.positive_active_image line 238
  11. theorem OAI.MixedCrossSeparation.activeConvertedGauss_eq_columnBlocks line 253
  12. theorem OAI.MixedCrossSeparation.activeConvertedGauss_disjoint_mod_four line 268
  13. abbrev OAI.FirstCauchyArithmetic.O line 287
  14. def OAI.FirstCauchyArithmetic.supportMobius line 290
  15. def OAI.FirstCauchyArithmetic.supportConjugateSum line 293
  16. theorem OAI.FirstCauchyArithmetic.supportMobius_union line 298
  17. theorem OAI.FirstCauchyArithmetic.supportMobius_sq line 306
  18. theorem OAI.FirstCauchyArithmetic.star_supportMobius line 313
  19. theorem OAI.FirstCauchyArithmetic.finiteSquarefreeRow_union line 317
  20. theorem OAI.FirstCauchyArithmetic.coprime_pair_sum_reindexed line 324
  21. theorem OAI.FirstCauchyArithmetic.finite_phase_coprime_reindex line 382
  22. def OAI.FirstCauchyArithmetic.supportRay line 444
  23. theorem OAI.FirstCauchyArithmetic.supportRay_union line 447
  24. theorem OAI.FirstCauchyArithmetic.supportConjugateSum_ray_common line 453
  25. theorem OAI.FirstCauchyArithmetic.supportConjugateSum_star_ray_common line 469
  26. theorem OAI.FirstCauchyArithmetic.quadratic_phase_coprime_ray_reindex line 485
  27. theorem OAI.FirstCauchyArithmetic.family_prime line 569
  28. theorem OAI.FirstCauchyArithmetic.family_prod_ne_zero line 572
  29. theorem OAI.FirstCauchyArithmetic.family_prime_dvd_product_iff line 576
  30. theorem OAI.FirstCauchyArithmetic.family_product_injective line 588
  31. def OAI.FirstCauchyArithmetic.supportIdealFamily line 596
  32. theorem OAI.FirstCauchyArithmetic.supportIdealFamily_pos line 600
  33. theorem OAI.FirstCauchyArithmetic.factor_family_product_iff line 607
  34. theorem OAI.FirstCauchyArithmetic.supportIdealFamily_good line 619
  35. def OAI.FirstCauchyArithmetic.recoveredSupport line 629
  36. theorem OAI.FirstCauchyArithmetic.recoveredSupport_product line 633
  37. theorem OAI.FirstCauchyArithmetic.idealSexticRow_support_product line 641
  38. theorem OAI.FirstCauchyArithmetic.supportConjugateSum_eq_conjugateIdealRowSum line 669
  39. theorem OAI.FirstCauchyArithmetic.quadratic_phase_reindex_to_ideal_rows line 691