OAI/GroupTheory/FiniteType/BinaryPrefixOperators.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinaryPrefixOperators.Space line 13
  2. def OAI.BinaryPrefixOperators.left line 15
  3. def OAI.BinaryPrefixOperators.right line 18
  4. lemma OAI.BinaryPrefixOperators.left_single line 22
  5. lemma OAI.BinaryPrefixOperators.right_single line 26
  6. lemma OAI.BinaryPrefixOperators.right_left line 31
  7. lemma OAI.BinaryPrefixOperators.partition line 40
  8. def OAI.BinaryPrefixOperators.algebra line 49
  9. instance OAI.BinaryPrefixOperators.algebraRing line 52
  10. def OAI.BinaryPrefixOperators.l line 55
  11. def OAI.BinaryPrefixOperators.r line 58
  12. lemma OAI.BinaryPrefixOperators.r_l line 61
  13. lemma OAI.BinaryPrefixOperators.l_r_partition line 65
  14. lemma OAI.BinaryPrefixOperators.r_l_mul line 75
  15. def OAI.BinaryPrefixOperators.sources line 80
  16. def OAI.BinaryPrefixOperators.targets line 86
  17. lemma OAI.BinaryPrefixOperators.targets_sources line 92
  18. def OAI.BinaryPrefixOperators.copy line 97
  19. lemma OAI.BinaryPrefixOperators.copy_diagonal line 100
  20. lemma OAI.BinaryPrefixOperators.first_one line 104
  21. lemma OAI.BinaryPrefixOperators.first_partition line 113
  22. def OAI.BinaryPrefixOperators.threeCopies line 122
  23. def OAI.BinaryPrefixOperators.idempotents line 131
  24. lemma OAI.BinaryPrefixOperators.identity_mem line 134
  25. lemma OAI.BinaryPrefixOperators.idempotents_are_idempotent line 136
  26. lemma OAI.BinaryPrefixOperators.idempotents_finite line 142
  27. lemma OAI.BinaryPrefixOperators.system_subset line 148
  28. theorem OAI.BinaryPrefixOperators.finite_idempotents line 153
  29. def OAI.BinaryPrefixOperators.AssignmentAdditive line 159
  30. theorem OAI.BinaryPrefixOperators.finite_idempotent_assignment line 164
  31. def OAI.ListChains.boundedBoundaries line 182
  32. lemma OAI.ListChains.fillsAt_iff_mem_boundaries line 185
  33. lemma OAI.ListChains.fillsAt_iff_quotient_zero line 194
  34. structure OAI.ListChains.IdempotentSplittings line 198
  35. theorem OAI.ListChains.IdempotentSplittings.uniform_nsmul_fillings line 209
  36. theorem OAI.ListChains.uniform_fillings_from_partial_homotopy line 253
  37. def OAI.ListChains.iterateHom line 272
  38. lemma OAI.ListChains.iterateHom_zero line 275
  39. lemma OAI.ListChains.iterateHom_one line 276
  40. lemma OAI.ListChains.iterateHom_add line 277
  41. def OAI.ListChains.UniformFillings line 285
  42. theorem OAI.ListChains.partial_homotopy_from_uniform line 290
  43. theorem OAI.ListChains.uniform_fillings_of_factorization_and_splittings line 311
  44. theorem OAI.ListChains.UniformFillings.families line 337
  45. theorem OAI.ListChains.UniformFillings.translated_families line 365
  46. def OAI.ListChains.cosetModule line 396
  47. lemma OAI.ListChains.single_mem_cosetModule line 402
  48. def OAI.ListChains.cosetMap line 410
  49. lemma OAI.ListChains.cosetMap_single line 414
  50. lemma OAI.ListChains.cosetMap_mem line 418
  51. lemma OAI.ListChains.cosetMap_comp line 430
  52. lemma OAI.ListChains.cosetMap_id line 441
  53. def OAI.ListChains.cosetBoundary line 448
  54. lemma OAI.ListChains.cosetBoundary_apply line 451
  55. lemma OAI.ListChains.cosetBoundary_single line 454
  56. lemma OAI.ListChains.cosetBoundary_squared line 459
  57. lemma OAI.ListChains.cosetBoundary_cosetMap line 462
  58. def OAI.ListChains.mergeCosets line 471
  59. lemma OAI.ListChains.mergeCosets_single line 474
  60. lemma OAI.ListChains.mergeCosets_eq line 478
  61. lemma OAI.ListChains.cosetBoundary_mergeCosets line 484