OAI/NumberTheory/DirichletL/PrimeRows/ActiveGaussFactorization.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ConcretePrimeRowBridge.idealRowSum_smoothed_summable line 64
  2. theorem OAI.ConcretePrimeRowBridge.idealRowSum_smoothed_expand line 78
  3. def OAI.ActualEisensteinCubic.activeSupport line 102
  4. abbrev OAI.ActualEisensteinCubic.activePrimes line 105
  5. def OAI.ActualEisensteinCubic.activeExponent line 108
  6. theorem OAI.ActualEisensteinCubic.activeExponent_ne_zero line 112
  7. theorem OAI.ActualEisensteinCubic.activeExponent_lt_six line 117
  8. theorem OAI.ActualEisensteinCubic.activePrimes_injective line 122
  9. theorem OAI.ActualEisensteinCubic.activePrimes_pairwise_isCoprime line 129
  10. theorem OAI.ActualEisensteinCubic.finiteSexticRow_activeSupport line 136
  11. theorem OAI.ActualEisensteinCubic.finiteSquarefreeRow_pair_activeSupport line 173
  12. def OAI.ActualEisensteinCubic.squarefreePairPoissonKernel line 186
  13. theorem OAI.ActualEisensteinCubic.finiteSquarefreeRow_pair_radial_poisson line 204
  14. def OAI.ConcretePrimeRowBridge.idealPairPoissonKernel line 230
  15. theorem OAI.ConcretePrimeRowBridge.idealRowSum_smoothed_poisson line 240
  16. theorem OAI.IdealGaussCRT.gauss_sum_finite_crt line 270
  17. abbrev OAI.FiniteGaussPhase.O line 293
  18. def OAI.FiniteGaussPhase.cofactor line 296
  19. theorem OAI.FiniteGaussPhase.prime_mul_cofactor line 299
  20. theorem OAI.FiniteGaussPhase.span_finset_prod line 303
  21. theorem OAI.FiniteGaussPhase.cofactor_coprime line 312
  22. def OAI.FiniteGaussPhase.productElementCRT line 318
  23. theorem OAI.FiniteGaussPhase.productElementCRT_mk line 324
  24. theorem OAI.FiniteGaussPhase.productElementCRT_axis line 332
  25. theorem OAI.FiniteGaussPhase.coordinate_trace_character line 356
  26. theorem OAI.FiniteGaussPhase.gauss_sum_product_element line 383
  27. def OAI.FiniteGaussPhase.normalizedProductTraceGauss line 402
  28. theorem OAI.FiniteGaussPhase.normalizedProductTraceGauss_crt line 414
  29. theorem OAI.FiniteGaussPhase.normalizedProductTraceGauss_cross_factors line 439
  30. def OAI.FiniteGaussPhase.canonicalProductGauss line 452
  31. theorem OAI.FiniteGaussPhase.canonicalProductGauss_cross_factors line 459
  32. theorem OAI.FiniteGaussPhase.canonicalProductGauss_constant_power line 472
  33. def OAI.FiniteGaussPhase.angularFactor line 488
  34. theorem OAI.FiniteGaussPhase.angularFactor_prod line 490
  35. def OAI.FiniteGaussPhase.canonicalCrossFactor line 495
  36. theorem OAI.FiniteGaussPhase.prime_generator_not_mem_other line 502
  37. theorem OAI.FiniteGaussPhase.canonicalCrossFactor_pow_six line 513
  38. def OAI.FiniteGaussPhase.canonicalProductCoefficient line 530
  39. theorem OAI.FiniteGaussPhase.canonicalProductCoefficient_crt line 537
  40. theorem OAI.FiniteGaussPhase.product_moebius_eq_sign line 552
  41. theorem OAI.FiniteGaussPhase.canonicalProductGauss_two_cube line 569
  42. def OAI.FiniteGaussPhase.canonicalProductG line 593
  43. theorem OAI.FiniteGaussPhase.canonicalProductGauss_one_two_relation line 602
  44. theorem OAI.FiniteGaussPhase.canonicalProductGauss_one_two_eq_moebius line 643
  45. theorem OAI.FiniteGaussPhase.norm_angularFactor line 658
  46. theorem OAI.FiniteGaussPhase.angularFactor_mul_star line 663
  47. theorem OAI.FiniteGaussPhase.norm_canonicalProductGauss line 668
  48. theorem OAI.FiniteGaussPhase.norm_canonicalProductG line 706
  49. theorem OAI.FiniteGaussPhase.canonicalProductCoefficient_mul_gauss_one line 724
  50. theorem OAI.FiniteGaussPhase.moebius_star_gauss_one_eq_coefficient line 750