OAI/NumberTheory/DirichletL/GaussSum/SexticNormalization.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ActualEisensteinCubic.breveGamma1 line 24
  2. def OAI.ActualEisensteinCubic.breveGamma3 line 32
  3. theorem OAI.ActualEisensteinCubic.canonicalSextic_pow_three_quadratic line 40
  4. theorem OAI.ActualEisensteinCubic.breveGamma1_gamma2_relation line 51
  5. theorem OAI.ActualEisensteinCubic.breveE_period_O line 118
  6. def OAI.ActualEisensteinCubic.eisBreveModChar line 129
  7. theorem OAI.ActualEisensteinCubic.eisEmbedding_traceLambda line 136
  8. theorem OAI.ActualEisensteinCubic.eisBreveModChar_eq_mulShift line 145
  9. def OAI.ActualEisensteinCubic.breveLocalG line 167
  10. theorem OAI.ActualEisensteinCubic.breveGamma1_gamma2_eq_neg_alpha_G line 173
  11. def OAI.ActualEisensteinCubic.breveGamma2Product line 189
  12. theorem OAI.ActualEisensteinCubic.breveGamma2Product_crt line 208
  13. def OAI.ConcreteBreveE.normalizedTraceGauss line 255
  14. def OAI.ConcreteBreveE.normalizedTraceGaussProduct line 262
  15. theorem OAI.ConcreteBreveE.normalizedTraceGaussProduct_crt line 277
  16. theorem OAI.FixedRayActiveSet.sum_zero_and_units line 315
  17. theorem OAI.FixedRayActiveSet.product_sum_by_active_set line 338
  18. theorem OAI.FixedRayActiveSet.branch_zero_of_local_mask line 360
  19. theorem OAI.FixedRayActiveSet.admissible_branch_count line 370
  20. theorem OAI.FixedRayActiveSet.branch_zero_outside_admissible line 380
  21. theorem OAI.FixedRayActiveSet.assemble_local_A5 line 395
  22. theorem OAI.CubeInversion.cube_index_filter_complex line 435
  23. theorem OAI.CubeInversion.cube_coefficient_filter line 443
  24. theorem OAI.CubeInversion.finite_cube_inversion line 472
  25. theorem OAI.CubeInversion.finite_cube_inversion_with_columns line 481
  26. def OAI.ActualEisensteinCubic.breveGammaMinus1 line 499
  27. theorem OAI.ActualEisensteinCubic.canonicalSextic_order_six line 507
  28. theorem OAI.ActualEisensteinCubic.breveGamma1_gammaMinus1 line 521
  29. theorem OAI.PowerExtraction.from_mean_square_and_prime_rows line 567