OAI/Combinatorics/Chromatic/Shuffle/PrimitiveUnitRows.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ElementaryPositivity.RawShuffle.SlopeStringStart line 18
  2. def OAI.ElementaryPositivity.RawShuffle.stringLetterStartEquiv line 21
  3. def OAI.ElementaryPositivity.RawShuffle.slopeStartParameter line 27
  4. def OAI.ElementaryPositivity.RawShuffle.slopeStartRowType line 31
  5. lemma OAI.ElementaryPositivity.RawShuffle.slopeStartEven_iff line 34
  6. def OAI.ElementaryPositivity.RawShuffle.primitiveCountEquiv line 41
  7. def OAI.ElementaryPositivity.RawShuffle.primitiveRowsEquiv line 48
  8. lemma OAI.ElementaryPositivity.RawShuffle.primitiveCount_energy line 52
  9. lemma OAI.ElementaryPositivity.RawShuffle.stringWord_dimension line 64
  10. lemma OAI.ElementaryPositivity.RawShuffle.primitiveCount_dimension line 71
  11. theorem OAI.ElementaryPositivity.RawShuffle.primitiveRows_energy line 80
  12. theorem OAI.ElementaryPositivity.RawShuffle.primitiveRows_dimension line 88
  13. lemma OAI.ElementaryPositivity.RawShuffle.strict_fin_nat_bound line 101
  14. def OAI.ElementaryPositivity.RawShuffle.weakStrictListEquiv line 113
  15. abbrev OAI.ElementaryPositivity.RawShuffle.UnitIndexList line 137
  16. def OAI.ElementaryPositivity.RawShuffle.weakUnitListEquiv line 139
  17. lemma OAI.ElementaryPositivity.RawShuffle.weakUnitListEquiv_val line 145
  18. lemma OAI.ElementaryPositivity.RawShuffle.fin_staircase_sum line 150
  19. abbrev OAI.ElementaryPositivity.RawShuffle.InputIndexLists line 161
  20. def OAI.ElementaryPositivity.RawShuffle.inputListEquiv line 162
  21. def OAI.ElementaryPositivity.RawShuffle.elementaryDiagonal line 165
  22. def OAI.ElementaryPositivity.RawShuffle.listIndexSum line 167
  23. lemma OAI.ElementaryPositivity.RawShuffle.inputListIndexSum line 170