OAI/Combinatorics/PolynomialVacuum/Pairing/PairingTarget.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.PolynomialVacuumCylinder.Vertex line 8
  2. abbrev OAI.PolynomialVacuumCylinder.Germ line 13
  3. abbrev OAI.PolynomialVacuumCylinder.Face line 14
  4. abbrev OAI.PolynomialVacuumCylinder.Edge line 15
  5. def OAI.PolynomialVacuumCylinder.neighbor line 17
  6. def OAI.PolynomialVacuumCylinder.edgeOf line 22
  7. def OAI.PolynomialVacuumCylinder.edgeVertices line 26
  8. def OAI.PolynomialVacuumCylinder.outgoingSlot line 29
  9. def OAI.PolynomialVacuumCylinder.advance line 30
  10. def OAI.PolynomialVacuumCylinder.traced line 33
  11. def OAI.PolynomialVacuumCylinder.terminalGerm line 37
  12. def OAI.PolynomialVacuumCylinder.tracedEdges line 41
  13. def OAI.PolynomialVacuumCylinder.IsPolygon line 45
  14. abbrev OAI.PolynomialVacuumCylinder.Polygon line 47
  15. def OAI.PolynomialVacuumCylinder.Polygon.vertices line 49
  16. def OAI.PolynomialVacuumCylinder.leftFace line 51
  17. def OAI.PolynomialVacuumCylinder.reverseGerm line 55
  18. def OAI.PolynomialVacuumCylinder.rightFace line 56
  19. def OAI.PolynomialVacuumCylinder.DualAdjacent line 58
  20. def OAI.PolynomialVacuumCylinder.Separates line 63
  21. def OAI.PolynomialVacuumCylinder.AllowedSystem line 66
  22. abbrev OAI.PolynomialVacuumCylinder.System line 69
  23. def OAI.PolynomialVacuumCylinder.systemWeight line 71
  24. def OAI.PolynomialVacuumCylinder.separatorPolynomial line 73
  25. def OAI.PolynomialVacuumCylinder.emptyCoefficient line 75
  26. def OAI.PolynomialVacuumCylinder.normalizedState line 77
  27. def OAI.PolynomialVacuumCylinder.blockCharge line 79
  28. def OAI.PolynomialVacuumCylinder.homogeneousContraction line 81
  29. abbrev OAI.PolynomialVacuumCylinder.AnalyticFamily line 87
  30. def OAI.PolynomialVacuumCylinder.AnalyticNormalization line 89
  31. def OAI.PolynomialVacuumCylinder.analyticHomogeneousContraction line 98
  32. def OAI.PolynomialVacuumCylinder.PhysicalSeparatorPairing line 105