OAI/Combinatorics/Chromatic/Walls/FiniteStringReordering.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ElementaryPositivity.RawShuffle.StringBlockIndex line 18
  2. def OAI.ElementaryPositivity.RawShuffle.homogeneousBStringEquiv line 21
  3. lemma OAI.ElementaryPositivity.RawShuffle.homogeneousBStringEquiv_degree line 28
  4. def OAI.ElementaryPositivity.RawShuffle.HNStringIndex line 31
  5. def OAI.ElementaryPositivity.RawShuffle.hnStringDegree line 35
  6. def OAI.ElementaryPositivity.RawShuffle.hnStringEquiv line 39
  7. lemma OAI.ElementaryPositivity.RawShuffle.hnStringEquiv_degree line 45
  8. abbrev OAI.ElementaryPositivity.RawShuffle.HNStringCoefficient line 56
  9. def OAI.ElementaryPositivity.RawShuffle.hnStringCoefficientEquiv line 60
  10. lemma OAI.ElementaryPositivity.RawShuffle.hnStringCoefficient_finite line 67
  11. theorem OAI.ElementaryPositivity.RawShuffle.finiteStringReordering_coefficient line 72
  12. def OAI.ElementaryPositivity.OrderedSignedWord line 84
  13. def OAI.ElementaryPositivity.SignedSelection line 85
  14. lemma OAI.ElementaryPositivity.count_le_one_of_signed_pairwise line 87
  15. lemma OAI.ElementaryPositivity.signed_pairwise_of_count line 100
  16. def OAI.ElementaryPositivity.signedWordSelectionEquiv line 123
  17. lemma OAI.ElementaryPositivity.signedWordSelectionEquiv_val line 138