OAI/NumberTheory/GaussianMoat/LatticeComponents.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianMoat.determinant line 7
  2. theorem OAI.GaussianMoat.determinant_mul_left line 9
  3. theorem OAI.GaussianMoat.norm_dvd_determinant line 14
  4. theorem OAI.GaussianMoat.determinant_eq_zero_of_common_factor line 21
  5. structure OAI.GaussianMoat.SplitSieve line 30
  6. def OAI.GaussianMoat.SplitSieve.avoiding line 38
  7. def OAI.GaussianMoat.FiniteSieveEndpoint line 41
  8. theorem OAI.GaussianMoat.finite_box line 46
  9. theorem OAI.GaussianMoat.finite_norm_le line 56
  10. theorem OAI.GaussianMoat.finite_irreducibles_divisible line 72
  11. def OAI.GaussianMoat.SplitSieve.exceptions line 78
  12. theorem OAI.GaussianMoat.SplitSieve.exceptions_finite line 81
  13. theorem OAI.GaussianMoat.SplitSieve.eventually_avoiding line 98
  14. theorem OAI.GaussianMoat.main_of_finiteSieve line 110
  15. theorem OAI.GaussianMoat.norm_square_complex line 123
  16. theorem OAI.GaussianMoat.finite_dist_le line 126
  17. theorem OAI.GaussianMoat.norm_le_of_dvd line 148
  18. theorem OAI.GaussianMoat.not_dvd_sub_of_dist_sq_lt line 159
  19. def OAI.GaussianMoat.latticeGraph line 167
  20. theorem OAI.GaussianMoat.lattice_walk_mem line 178
  21. theorem OAI.GaussianMoat.lattice_walk_dist line 187
  22. structure OAI.GaussianMoat.LatticePrefix line 202
  23. theorem OAI.GaussianMoat.LatticePrefix.dist_le line 209
  24. instance OAI.GaussianMoat.LatticePrefix.finite line 224
  25. def OAI.GaussianMoat.LatticePrefix.restrict line 235
  26. theorem OAI.GaussianMoat.infinite_component_has_walk line 243
  27. theorem OAI.GaussianMoat.lattice_component_finite line 297
  28. def OAI.GaussianMoat.latticeTranslation line 306
  29. theorem OAI.GaussianMoat.eq_of_finite_component_period line 315
  30. def OAI.GaussianMoat.SplitSieve.period line 343
  31. theorem OAI.GaussianMoat.SplitSieve.period_pos line 345
  32. theorem OAI.GaussianMoat.SplitSieve.factor_dvd_period line 348
  33. theorem OAI.GaussianMoat.SplitSieve.periodic line 364
  34. def OAI.GaussianMoat.residue line 378
  35. theorem OAI.GaussianMoat.eq_add_period_of_residue_eq line 380
  36. theorem OAI.GaussianMoat.periodic_component_bound line 391
  37. def OAI.GaussianMoat.SplitSieve.boundary line 408
  38. theorem OAI.GaussianMoat.SplitSieve.boundary_finite line 411
  39. def OAI.GaussianMoat.SplitSieve.restored line 416
  40. theorem OAI.GaussianMoat.SplitSieve.restored_finite line 419
  41. theorem OAI.GaussianMoat.lattice_reachable_mem line 424
  42. theorem OAI.GaussianMoat.SplitSieve.restored_closed line 430
  43. theorem OAI.GaussianMoat.prime_reachable_mem line 448
  44. theorem OAI.GaussianMoat.lattice_component_eq_singleton line 458
  45. theorem OAI.GaussianMoat.SplitSieve.component_subset line 473
  46. theorem OAI.GaussianMoat.prime_components_of_finiteSieve line 495
  47. theorem OAI.GaussianMoat.finite_prime_walk_bound line 525
  48. theorem OAI.GaussianMoat.endpoints_of_finiteSieve line 550