OAI/Combinatorics/Chromatic/Shuffle/PrimitiveBlockRows.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.blockWordEquiv line 18
  2. abbrev OAI.ElementaryPositivity.RawShuffle.BlockRows line 40
  3. def OAI.ElementaryPositivity.RawShuffle.blockRowsEquiv line 45
  4. def OAI.ElementaryPositivity.RawShuffle.blockRowsEnergy line 50
  5. lemma OAI.ElementaryPositivity.RawShuffle.blockRowsEquiv_energy line 54
  6. def OAI.ElementaryPositivity.RawShuffle.HNRowsIndex line 60
  7. def OAI.ElementaryPositivity.RawShuffle.hnRowsEquiv line 64
  8. def OAI.ElementaryPositivity.RawShuffle.hnRowsEnergy line 68
  9. lemma OAI.ElementaryPositivity.RawShuffle.hnRowsEquiv_energy line 73
  10. def OAI.ElementaryPositivity.RawShuffle.outputRowsEquiv line 83
  11. lemma OAI.ElementaryPositivity.RawShuffle.outputRows_admissible line 88
  12. def OAI.ElementaryPositivity.RawShuffle.outputRowsSeries line 93
  13. theorem OAI.ElementaryPositivity.RawShuffle.finiteReordering_rows line 96
  14. abbrev OAI.ElementaryPositivity.RawShuffle.RowBlock line 116
  15. def OAI.ElementaryPositivity.RawShuffle.rowsDecorate line 118
  16. lemma OAI.ElementaryPositivity.RawShuffle.rowsDecorate_dim line 122
  17. def OAI.ElementaryPositivity.RawShuffle.rowsUndecorate line 128
  18. lemma OAI.ElementaryPositivity.RawShuffle.rowsDecorate_undecorate line 132
  19. lemma OAI.ElementaryPositivity.RawShuffle.rowsDecorate_injective line 140
  20. def OAI.ElementaryPositivity.RawShuffle.rowsCons line 151
  21. lemma OAI.ElementaryPositivity.RawShuffle.rowsUndecorate_decorate line 155
  22. abbrev OAI.ElementaryPositivity.RawShuffle.DecoratedHN line 166
  23. def OAI.ElementaryPositivity.RawShuffle.decorateOutput line 169
  24. def OAI.ElementaryPositivity.RawShuffle.decoratedDimension line 178
  25. def OAI.ElementaryPositivity.RawShuffle.decoratedEnergy line 180
  26. lemma OAI.ElementaryPositivity.RawShuffle.decoratedEnergy_rows line 185
  27. lemma OAI.ElementaryPositivity.RawShuffle.decoratedDimension_append line 192
  28. lemma OAI.ElementaryPositivity.RawShuffle.decoratedEnergy_append line 196
  29. lemma OAI.ElementaryPositivity.RawShuffle.decoratedEnergy_admissible line 208