OAI/NumberTheory/DirichletL/GaussSum/CubicTrace.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ActualEisensteinCubic.cubicChar_reduce_ne_one line 68
  2. theorem OAI.ActualEisensteinCubic.cubicGauss_cube_of_nontrivial line 82
  3. theorem OAI.ActualEisensteinCubic.cubicGauss_cube_reduce line 129
  4. theorem OAI.CubicFrobenius.card_cast_ne_zero line 145
  5. theorem OAI.CubicFrobenius.gaussSum_pow_card line 155
  6. theorem OAI.CubicFrobenius.gauss_cube_residue_relation line 175
  7. theorem OAI.ActualEisensteinCubic.cubic_primary_frobenius_relation line 207
  8. theorem OAI.ActualEisensteinCubic.cubic_reciprocity_distinct_residue_char line 274
  9. theorem OAI.ActualEisensteinCubic.canonicalSextic_sq_reciprocity_distinct_residue_char line 297
  10. abbrev OAI.GaussGeneratorTransport.O line 322
  11. theorem OAI.GaussGeneratorTransport.norm_eisEmbedding_unit line 325
  12. theorem OAI.GaussGeneratorTransport.norm_eisEmbedding_unit_mul line 330
  13. theorem OAI.GaussGeneratorTransport.finiteSexticRow_unit_mul_star line 334
  14. def OAI.GaussGeneratorTransport.principalNormalizedGauss line 345
  15. theorem OAI.GaussGeneratorTransport.canonicalNormalizedGauss_eq_principal line 356
  16. theorem OAI.GaussGeneratorTransport.principal_gauss_sum_unit_change line 364
  17. theorem OAI.GaussGeneratorTransport.principalNormalizedGauss_unit_change line 400
  18. theorem OAI.GaussGeneratorTransport.principalNormalizedGauss_eq_product line 418
  19. theorem OAI.GaussGeneratorTransport.exists_modulus_unit line 427
  20. def OAI.GaussGeneratorTransport.modulusUnit line 435
  21. theorem OAI.GaussGeneratorTransport.modulusUnit_spec line 438
  22. theorem OAI.GaussGeneratorTransport.canonicalNormalizedGauss_eq_product line 442
  23. theorem OAI.GaussGeneratorTransport.canonicalNormalizedGauss_frequency_transport line 457
  24. theorem OAI.GaussGeneratorTransport.gauss_weighted_radial_sum_transport line 475
  25. theorem OAI.GaussGeneratorTransport.gauss_weighted_finite_radial_sum_transport line 498
  26. theorem OAI.GaussGeneratorTransport.finitePrimeModulus_norm_eq_product line 521
  27. theorem OAI.GaussGeneratorTransport.canonical_radial_poisson_product line 526
  28. theorem OAI.GaussGeneratorTransport.moebius_star_canonicalNormalizedGauss line 556
  29. theorem OAI.GaussGeneratorTransport.moebius_gauss_frequency_conversion line 574
  30. def OAI.GaussGeneratorTransport.squarefreePairProductPoissonKernel line 600
  31. theorem OAI.GaussGeneratorTransport.squarefreePairPoissonKernel_eq_product line 621
  32. theorem OAI.GaussGeneratorTransport.finiteSquarefreeRow_pair_radial_poisson_product line 663