OAI/NumberTheory/DirichletL/Arithmetic/LatticeCount.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ShortDraftLatticeCount.q line 20
  2. theorem OAI.ShortDraftLatticeCount.coordinate_squares line 22
  3. theorem OAI.ShortDraftLatticeCount.finite_lattice_count line 27
  4. theorem OAI.ShortDraftLatticeCount.finite_lattice_count_linear line 56
  5. theorem OAI.ShortDraftLatticeCount.actual_eisenstein_count line 66
  6. theorem OAI.ActualEisensteinCubic.A3_cubicChar_neg_one line 98
  7. theorem OAI.ActualEisensteinCubic.A3_ramified_local_character line 111
  8. theorem OAI.ActualEisensteinCubic.A3_ramified_reciprocity_local_character line 126
  9. theorem OAI.ActualEisensteinCubic.A3_unramified_local_character line 142
  10. theorem OAI.ShortDraftCusp.A3_coprime_a_c line 166
  11. theorem OAI.ShortDraftCusp.A3_coprime_a_b line 171
  12. theorem OAI.ShortDraftCusp.A3_ramified_coprime_a_A line 176
  13. theorem OAI.ShortDraftCusp.A3_unramified_coprime_a_minus_b line 182
  14. theorem OAI.ShortDraftLatticeCount.coords_eval line 193
  15. theorem OAI.ShortDraftLatticeCount.qO_mul line 198
  16. theorem OAI.ShortDraftLatticeCount.qO_nonneg line 211
  17. theorem OAI.ShortDraftLatticeCount.qO_pos line 214
  18. def OAI.ShortDraftLatticeCount.qNat line 225
  19. theorem OAI.ShortDraftLatticeCount.qNat_mul line 227
  20. theorem OAI.ShortDraftLatticeCount.qNat_pos line 232
  21. theorem OAI.ShortDraftLatticeCount.finite_multiples_count line 238
  22. def OAI.AnalyticBridge.CRTChoice.childPair line 260
  23. theorem OAI.AnalyticBridge.second_passage_weighted_fiber line 263
  24. theorem OAI.AnalyticBridge.second_passage_positive_reassembly line 291
  25. theorem OAI.ShortDraftLatticeCount.finite_divisible_count line 341
  26. theorem OAI.IdealGaussCRT.leftAddChar_mulShift line 376
  27. theorem OAI.IdealGaussCRT.rightAddChar_mulShift line 387
  28. theorem OAI.IdealGaussCRT.gauss_transform_crt line 398
  29. theorem OAI.IdealGaussCRT.gauss_transform_ideal_crt line 428
  30. theorem OAI.ActualEisensteinCubic.prime_sixth_row_approx line 465
  31. theorem OAI.ActualEisensteinCubic.prime_sixth_row_approx_maximal line 503
  32. theorem OAI.ActualEisensteinCubic.canonical_two_prime_gauss_transform line 531