OAI/NumberTheory/DirichletL/Eisenstein/PrimeGaussFactors.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.unramifiedCubicGaussSeries_prime_two_power line 87
  2. lemma OAI.CubicEisenstein.unramifiedCubicGaussSeries_square_cube line 110
  3. theorem OAI.CubicEisenstein.unramifiedGaussResidue_square_cube line 120
  4. lemma OAI.CubicEisenstein.principalResidueTerm_square_cube line 136
  5. lemma OAI.CubicEisenstein.principalArithmeticResidue_square_cube line 155
  6. theorem OAI.CubicEisenstein.sourceArithmeticResidue_square_cube line 166
  7. lemma OAI.CubicEisenstein.sourceArithmeticResidue_prime_pow_mod line 193
  8. theorem OAI.CubicEisenstein.sourceArithmeticResidue_prime_square line 207
  9. theorem OAI.CubicEisenstein.sourceArithmeticResidue_prime_factor line 220
  10. theorem OAI.CubicEisenstein.sourceArithmeticResidue_prime_power_table line 259
  11. lemma OAI.CubicEisenstein.primeCubicMulChar_inverse line 282
  12. lemma OAI.CubicEisenstein.primeCubicGauss_two_eq_star line 287
  13. lemma OAI.CubicEisenstein.primeCubicGauss_one_normalized line 302
  14. lemma OAI.CubicEisenstein.primeCubicGauss_two_twist line 317
  15. lemma OAI.CubicEisenstein.cubicBesselNormalizer_mul line 339
  16. lemma OAI.CubicEisenstein.prime_normalizer_powers line 350
  17. theorem OAI.CubicEisenstein.sourceResidualFourierCoefficient_prime_factor line 359
  18. theorem OAI.CubicEisenstein.sourceResidualFourierCoefficient_prime_gamma line 370
  19. def OAI.CubicEisenstein.normalizedCubicUnitGauss line 390
  20. lemma OAI.CubicEisenstein.normalizedCubicUnitGauss_one line 393
  21. lemma OAI.CubicEisenstein.cubicSymbol_star_mul line 396
  22. lemma OAI.CubicEisenstein.normalizedCubicUnitGauss_coprime_product line 407
  23. lemma OAI.CubicEisenstein.sourceResidualFourierCoefficient_prime_normalized line 433
  24. lemma OAI.CubicEisenstein.primary_finset_product line 446
  25. theorem OAI.CubicEisenstein.sourceResidualFourierCoefficient_prime_product line 456
  26. lemma OAI.CubicEisenstein.symbol_nine_eq_paperLambda line 492
  27. theorem OAI.CubicEisenstein.sourceResidualFourierCoefficient_primary_product line 502
  28. theorem OAI.CubicEisenstein.sourceArithmeticResidue_primary_cube line 522
  29. theorem OAI.CubicEisenstein.sourceResidualFourierCoefficient_primary_cube line 540
  30. lemma OAI.CubicEisenstein.cubicSymbol_prime_zero line 556
  31. lemma OAI.CubicEisenstein.cubicSymbol_zero_of_not_coprime line 564
  32. lemma OAI.CubicEisenstein.cubicRow_eq_idealSymbol line 581
  33. lemma OAI.CubicEisenstein.cubicUnitGaussSum_full line 599
  34. theorem OAI.CubicEisenstein.normalizedCubicUnitGauss_eq_gaussTwo line 625