OAI/Combinatorics/FiniteCircle/Translations.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteCircle.editDistance_append_le line 11
  2. theorem OAI.FiniteCircle.editDistance_flatMap_le line 16
  3. theorem OAI.FiniteCircle.editDistance_flatMap_uniform line 24
  4. theorem OAI.FiniteCircle.editDistance_ofFn_le_hamming line 36
  5. theorem OAI.FiniteCircle.ed_halfBit_le line 62
  6. theorem OAI.FiniteCircle.ed_tagged_halfBit_le line 67
  7. theorem OAI.FiniteCircle.editDistance_shifted_rows line 83
  8. theorem OAI.FiniteCircle.editDistance_flatMap_scaled line 109
  9. theorem OAI.FiniteCircle.tree_cheap_ed line 122
  10. def OAI.FiniteCircle.treeCopies line 195
  11. theorem OAI.FiniteCircle.tree_coordinate_ed line 199
  12. theorem OAI.FiniteCircle.tree_single_ed line 234
  13. theorem OAI.FiniteCircle.tree_length_eq line 256
  14. theorem OAI.FiniteCircle.residue_representative line 266
  15. theorem OAI.FiniteCircle.mask_CRT_shift line 282
  16. theorem OAI.FiniteCircle.excluded_CRT_shift line 299
  17. def OAI.FiniteCircle.flatMaskWord line 316
  18. def OAI.FiniteCircle.flatExcludedWord line 320
  19. theorem OAI.FiniteCircle.flatMaskWord_succ line 324
  20. theorem OAI.FiniteCircle.flatExcludedWord_succ line 337
  21. theorem OAI.FiniteCircle.mask_cheap_ed line 353
  22. theorem OAI.FiniteCircle.excluded_cheap_ed line 365
  23. theorem OAI.FiniteCircle.sum_map_maskTags line 377
  24. theorem OAI.FiniteCircle.sum_map_excludedTags line 383
  25. theorem OAI.FiniteCircle.flatMaskWord_base line 387
  26. theorem OAI.FiniteCircle.flatExcludedWord_base line 392
  27. theorem OAI.FiniteCircle.mask_single_ed line 397
  28. theorem OAI.FiniteCircle.excluded_single_ed line 408