OAI/Combinatorics/Chromatic/Witness/ElementarySingletonCoefficient.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.ElementaryMatrix.allOnes line 15
  2. lemma OAI.ElementaryPositivity.ElementaryMatrix.allOnes_apply line 16
  3. lemma OAI.ElementaryPositivity.ElementaryMatrix.allOnes_degree line 17
  4. lemma OAI.ElementaryPositivity.ElementaryMatrix.singleton_coefficient line 22
  5. lemma OAI.ElementaryPositivity.ElementaryMatrix.profile_multinomial_pos line 30
  6. def OAI.ElementaryPositivity.TriangularDynamics.historyDimension line 43
  7. def OAI.ElementaryPositivity.TriangularDynamics.historySyntax line 45
  8. lemma OAI.ElementaryPositivity.TriangularDynamics.historySyntax_positive line 50
  9. abbrev OAI.ElementaryPositivity.TriangularDynamics.HistoryLeaf line 55
  10. def OAI.ElementaryPositivity.TriangularDynamics.historyProfile line 56
  11. lemma OAI.ElementaryPositivity.TriangularDynamics.historyProfile_degree line 57
  12. lemma OAI.ElementaryPositivity.TriangularDynamics.historyProfile_dominant line 59
  13. def OAI.ElementaryPositivity.TriangularDynamics.historyWeight line 63
  14. lemma OAI.ElementaryPositivity.TriangularDynamics.historyWeight_positive line 67
  15. lemma OAI.ElementaryPositivity.TriangularDynamics.history_coefficient line 70
  16. lemma OAI.ElementaryPositivity.TriangularDynamics.history_singleton line 79
  17. lemma OAI.ElementaryPositivity.TriangularDynamics.historyWeight_support line 91