OAI/Combinatorics/CompleteCrossing/CycleIdentity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The geometric cycle identity deduced from endpoint and intersection coordinates.

  1. theorem OAI.Paper170.endpointSign_eq_sub_indicators line 17
  2. theorem OAI.Paper170.sum_endpointSign line 25
  3. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.flagPairing_eq_spokeComparison line 38
  4. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.edgeEndpointPairing_eq_signed_sum line 49
  5. theorem OAI.Paper170Geometry.TruncatedSpokeCoordinates.cycleMatrix_pairing_zero line 80
  6. theorem OAI.Paper170.cycle_pairing_of_coordinates line 106
  7. theorem OAI.Paper170.cycle_pairing line 133
  8. theorem OAI.Paper170.raw_cycle_pairing line 141