OAI/NumberTheory/TwoPoint/Walks/ClosedPathProduct.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Join two paths with common endpoints into the literal closed signed word.

  1. lemma OAI.TwoPointCorrelations.scalarWalkProduct_append line 9
  2. lemma OAI.TwoPointCorrelations.scalarWalkProduct_reverse line 21
  3. theorem OAI.TwoPointCorrelations.scalarWalkProduct_closed_pair line 39
  4. theorem OAI.TwoPointCorrelations.signedIntegerWeight_closed_pair line 47