OAI/Combinatorics/Chromatic/QuantumTorus/Admissible.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ElementaryPositivity.NaturalUnitIntervalGraph.edge_comm line 10
  2. theorem OAI.ElementaryPositivity.NaturalUnitIntervalGraph.edge_irrefl line 13
  3. def OAI.ElementaryPositivity.NaturalUnitIntervalGraph.Admissible line 16
  4. instance OAI.ElementaryPositivity.NaturalUnitIntervalGraph.(instance at line 19) line 19
  5. def OAI.ElementaryPositivity.NaturalUnitIntervalGraph.reversePerm line 23
  6. theorem OAI.ElementaryPositivity.NaturalUnitIntervalGraph.reversePerm_apply line 26
  7. theorem OAI.ElementaryPositivity.NaturalUnitIntervalGraph.reversePerm_reverse line 29
  8. lemma OAI.ElementaryPositivity.NaturalUnitIntervalGraph.rev_adjacent line 34
  9. theorem OAI.ElementaryPositivity.NaturalUnitIntervalGraph.nondescent_iff_reverse_admissible line 39
  10. def OAI.ElementaryPositivity.NaturalUnitIntervalGraph.reversalEquiv line 48
  11. def OAI.ElementaryPositivity.NaturalUnitIntervalGraph.edges line 56
  12. def OAI.ElementaryPositivity.NaturalUnitIntervalGraph.edgeCount line 59
  13. def OAI.ElementaryPositivity.NaturalUnitIntervalGraph.invertedEdges line 61
  14. lemma OAI.ElementaryPositivity.NaturalUnitIntervalGraph.mem_edges line 64
  15. lemma OAI.ElementaryPositivity.NaturalUnitIntervalGraph.mem_invertedEdges line 67
  16. theorem OAI.ElementaryPositivity.NaturalUnitIntervalGraph.graphInversions_eq_card_invertedEdges line 72
  17. theorem OAI.ElementaryPositivity.NaturalUnitIntervalGraph.inverse_reverse_apply line 92
  18. lemma OAI.ElementaryPositivity.NaturalUnitIntervalGraph.invertedEdges_reverse line 95
  19. theorem OAI.ElementaryPositivity.NaturalUnitIntervalGraph.graphInversions_add_reverse line 108
  20. theorem OAI.ElementaryPositivity.NaturalUnitIntervalGraph.graphInversions_le_edges line 114
  21. theorem OAI.ElementaryPositivity.NaturalUnitIntervalGraph.graphInversions_reverse line 119
  22. def OAI.ElementaryPositivity.NaturalUnitIntervalGraph.coloringInversions line 124
  23. def OAI.ElementaryPositivity.NaturalUnitIntervalGraph.inversionChromatic line 127
  24. lemma OAI.ElementaryPositivity.NaturalUnitIntervalGraph.coloringAscents_eq_card line 132
  25. theorem OAI.ElementaryPositivity.NaturalUnitIntervalGraph.coloringInversions_add_ascents line 139
  26. def OAI.ElementaryPositivity.CoefficientReflection.reflectPolynomial line 156
  27. def OAI.ElementaryPositivity.CoefficientReflection.reflect line 161
  28. theorem OAI.ElementaryPositivity.CoefficientReflection.coeff_reflect line 167
  29. theorem OAI.ElementaryPositivity.CoefficientReflection.reflect_C_X_pow_mul_map line 172
  30. lemma OAI.ElementaryPositivity.CoefficientReflection.map_esymmPart line 182
  31. theorem OAI.ElementaryPositivity.CoefficientReflection.reflect_C_X_pow_mul_esymmPart line 188
  32. theorem OAI.ElementaryPositivity.NaturalUnitIntervalGraph.reflect_inversionChromatic line 202