OAI/Combinatorics/SumProduct/Alignment/IntegerAlignment01.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RoughArrayFace.source_raw_physical_array_own_face_decay line 26
  2. lemma OAI.IntegerAlignment.fixed_dvd_primorial_pow line 100
  3. lemma OAI.IntegerAlignment.fixed_mul_primorial_dvd line 112
  4. lemma OAI.IntegerAlignment.finite_absorption line 119
  5. def OAI.IntegerAlignment.Smooth line 128
  6. def OAI.IntegerAlignment.Rough line 130
  7. lemma OAI.IntegerAlignment.coprime_smooth_rough line 132
  8. lemma OAI.IntegerAlignment.primorial_smooth line 139
  9. lemma OAI.IntegerAlignment.coprime_modulus line 143
  10. lemma OAI.IntegerAlignment.integral_translation line 149
  11. lemma OAI.IntegerAlignment.residue_shift line 160
  12. lemma OAI.IntegerAlignment.residue_unique line 196
  13. lemma OAI.IntegerAlignment.own_target_reading line 208
  14. lemma OAI.IntegerAlignment.terminal_translation line 225
  15. structure OAI.IntegerAlignment.ResidueData line 236
  16. theorem OAI.IntegerAlignment.residue_system line 252
  17. lemma OAI.IntegerAlignment.fixed_dvd_delta line 270
  18. lemma OAI.IntegerAlignment.rough_slot line 278
  19. lemma OAI.IntegerAlignment.model_array_exponent line 292