OAI/Combinatorics/SumProduct/Alignment/AllLevel04.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.AllLevelRemovals.Removal line 30
  2. def OAI.AllLevelRemovals.Removal.left line 47
  3. def OAI.AllLevelRemovals.Removal.right line 50
  4. lemma OAI.AllLevelRemovals.Removal.flow_int line 54
  5. lemma OAI.AllLevelRemovals.Removal.right_eq line 60
  6. def OAI.AllLevelRemovals.Removal.reindex line 65
  7. lemma OAI.AllLevelRemovals.Removal.reindex_left line 82
  8. lemma OAI.AllLevelRemovals.Removal.reindex_right line 85
  9. def OAI.AllLevelRemovals.leftWord line 90
  10. def OAI.AllLevelRemovals.rightWord line 93
  11. lemma OAI.AllLevelRemovals.leftWord_nil line 97
  12. lemma OAI.AllLevelRemovals.rightWord_nil line 99
  13. lemma OAI.AllLevelRemovals.leftWord_append line 102
  14. lemma OAI.AllLevelRemovals.rightWord_append line 106
  15. lemma OAI.AllLevelRemovals.leftWord_reindex line 111
  16. lemma OAI.AllLevelRemovals.rightWord_reindex line 117
  17. structure OAI.AllLevelStates.State line 144
  18. def OAI.AllLevelStates.State.Irrational line 160
  19. lemma OAI.AllLevelStates.State.monoidHom_word line 170
  20. lemma OAI.AllLevelStates.State.lift_coefficients line 179
  21. theorem OAI.AllLevelStates.State.descend_integral line 240