OAI/Geometry/PeriodicTiling/PlaneLattices.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PeriodicTilingThree.Period.zsmul line 24
  2. theorem OAI.PeriodicTilingThree.Period.nsmul line 27
  3. theorem OAI.PeriodicTilingThree.exists_pos_zsmul_mem line 30
  4. def OAI.PeriodicTilingThree.bezoutCoordinates line 38
  5. theorem OAI.PeriodicTilingThree.exists_primitive_coordinates line 67
  6. def OAI.PeriodicTilingThree.coordinateSubgroup line 88
  7. theorem OAI.PeriodicTilingThree.index_coordinateSubgroup line 91
  8. theorem OAI.PeriodicTilingThree.coordinateSubgroup_le line 96
  9. theorem OAI.PeriodicTilingThree.finiteIndex_of_coordinate_mem line 108
  10. theorem OAI.PeriodicTilingThree.FullyPeriodic.exists_coordinate_period line 117
  11. theorem OAI.PeriodicTilingThree.fullyPeriodic_of_coordinate_periods line 130
  12. theorem OAI.PeriodicTilingThree.Period.mem_coordinate_mod line 138
  13. def OAI.PeriodicTilingThree.planeDet line 151
  14. theorem OAI.PeriodicTilingThree.planeDet_self line 153
  15. theorem OAI.PeriodicTilingThree.planeDet_swap line 156
  16. theorem OAI.PeriodicTilingThree.planeDet_zsmul_left line 160
  17. theorem OAI.PeriodicTilingThree.planeDet_zsmul_right line 165
  18. theorem OAI.PeriodicTilingThree.zsmul_plane_ne_zero line 170
  19. def OAI.PeriodicTilingThree.integerCombination line 182
  20. def OAI.PeriodicTilingThree.integerSpan2 line 192
  21. theorem OAI.PeriodicTilingThree.mem_integerSpan2 line 194
  22. theorem OAI.PeriodicTilingThree.determinant_smul_eq line 202
  23. theorem OAI.PeriodicTilingThree.integerSpan2_finiteIndex line 212
  24. theorem OAI.PeriodicTilingThree.fullyPeriodic_of_independent_periods line 222
  25. theorem OAI.PeriodicTilingThree.exists_smul_eq_of_collinear line 229
  26. theorem OAI.PeriodicTilingThree.planeDet_zero_trans line 256
  27. theorem OAI.PeriodicTilingThree.exists_common_collinear_multiple line 266
  28. theorem OAI.PeriodicTilingThree.exists_transverse_vector line 291
  29. theorem OAI.PeriodicTilingThree.exists_common_transverse line 310
  30. theorem OAI.PeriodicTilingThree.exists_common_second_vector line 336