OAI/NumberTheory/DirichletL/Arithmetic/EisensteinCoordinates.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ShortDraft.eisenstein_ring_pid line 197
  2. abbrev OAI.ShortDraft.EisensteinCoordinates line 203
  3. def OAI.ShortDraft.eisensteinMul line 205
  4. def OAI.ShortDraft.eisensteinConj line 208
  5. def OAI.ShortDraft.eisensteinNorm line 211
  6. theorem OAI.ShortDraft.eisenstein_norm_mul line 214
  7. theorem OAI.ShortDraft.eisenstein_norm_conj line 221
  8. theorem OAI.ShortDraft.eisenstein_mul_conj line 227
  9. theorem OAI.ShortDraft.eisenstein_norm_nonneg line 232
  10. theorem OAI.ShortDraft.eisenstein_norm_eq_zero_iff line 238
  11. def OAI.ShortDraft.DirichletTarget line 253
  12. theorem OAI.ShortDraft.dirichlet_target_of_one_le_re line 258
  13. theorem OAI.ShortDraft.dirichletTarget_iff_open_strip line 264
  14. theorem OAI.ShortDraft.cube_index_filter line 279
  15. lemma OAI.ShortDraft.square_le_two_squares line 288
  16. theorem OAI.ShortDraft.finite_row_extraction line 297
  17. theorem OAI.ShortDraft.complex_row_extraction line 328
  18. theorem OAI.ShortDraft.mean_square_exponent line 348
  19. theorem OAI.ShortDraft.approximation_exponent line 351
  20. theorem OAI.ShortDraft.zero_free_of_analytic_identity line 354
  21. theorem OAI.ShortDraft.zero_free_of_regularized_analytic_identity line 377
  22. theorem OAI.ShortDraft.two_poisson_scale_substitution line 399
  23. theorem OAI.ShortDraft.two_poisson_budget line 421
  24. theorem OAI.ShortDraft.two_poisson_charge line 468
  25. theorem OAI.ShortDraft.two_poisson_cost_identity line 490
  26. theorem OAI.ShortDraftLocal.sextic_character_exponent line 515
  27. theorem OAI.ShortDraftLocal.gaussSum_mulShift_any line 525
  28. theorem OAI.ShortDraftLocal.gaussSum_eq_units_sum line 538
  29. theorem OAI.ShortDraftLocal.sextic_character_quadratic line 559
  30. theorem OAI.ShortDraftLocal.sextic_inversion_sum line 569
  31. theorem OAI.ShortDraftLocal.sextic_inversion_gaussSum line 592
  32. theorem OAI.ShortDraftLocal.sextic_local_row line 599
  33. theorem OAI.ShortDraftLocal.additive_unit_sum line 608
  34. theorem OAI.ShortDraftLocal.sextic_fourth_mask line 627
  35. theorem OAI.ShortDraftLocal.active_zero_local_row line 647
  36. theorem OAI.ShortDraftLocal.nontrivial_fourier_coefficient line 670
  37. theorem OAI.ShortDraftLocal.trivial_fourier_coefficient line 685
  38. theorem OAI.ShortDraftLocal.sextic_fourier_theta_row line 703