OAI/Geometry/PeriodicTiling/EncodingParameters.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PeriodicTilingThree.PrimeTag line 12
  2. structure OAI.PeriodicTilingThree.EncodingParameters line 15
  3. def OAI.PeriodicTilingThree.EncodingParameters.a line 36
  4. def OAI.PeriodicTilingThree.EncodingParameters.b line 37
  5. def OAI.PeriodicTilingThree.EncodingParameters.digitPrime line 38
  6. theorem OAI.PeriodicTilingThree.EncodingParameters.a_prime line 41
  7. theorem OAI.PeriodicTilingThree.EncodingParameters.b_prime line 42
  8. theorem OAI.PeriodicTilingThree.EncodingParameters.digitPrime_prime line 43
  9. theorem OAI.PeriodicTilingThree.EncodingParameters.a_pos line 46
  10. theorem OAI.PeriodicTilingThree.EncodingParameters.b_pos line 47
  11. theorem OAI.PeriodicTilingThree.EncodingParameters.digitPrime_pos line 48
  12. theorem OAI.PeriodicTilingThree.EncodingParameters.a_two_le line 51
  13. theorem OAI.PeriodicTilingThree.EncodingParameters.b_two_le line 52
  14. theorem OAI.PeriodicTilingThree.EncodingParameters.seed_a line 54
  15. theorem OAI.PeriodicTilingThree.EncodingParameters.digit_eq line 56
  16. theorem OAI.PeriodicTilingThree.EncodingParameters.prime_coprime line 60
  17. theorem OAI.PeriodicTilingThree.EncodingParameters.prime_coprime_p line 65
  18. theorem OAI.PeriodicTilingThree.EncodingParameters.a_coprime_b line 68
  19. theorem OAI.PeriodicTilingThree.EncodingParameters.digitPrime_pairwise line 72
  20. def OAI.PeriodicTilingThree.EncodingParameters.r line 83
  21. theorem OAI.PeriodicTilingThree.EncodingParameters.r_pos line 85
  22. instance OAI.PeriodicTilingThree.EncodingParameters.a_neZero line 88
  23. instance OAI.PeriodicTilingThree.EncodingParameters.b_neZero line 89
  24. instance OAI.PeriodicTilingThree.EncodingParameters.digitPrime_neZero line 90
  25. instance OAI.PeriodicTilingThree.EncodingParameters.r_neZero line 92
  26. theorem OAI.PeriodicTilingThree.EncodingParameters.r_coprime_a line 94
  27. theorem OAI.PeriodicTilingThree.EncodingParameters.r_coprime_b line 100
  28. theorem OAI.PeriodicTilingThree.EncodingParameters.r_coprime_p line 106
  29. theorem OAI.PeriodicTilingThree.EncodingParameters.r_pairwise_coprime line 111