OAI/NumberTheory/TwoPoint/Walks/ClosedTraceSummation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Partition the actual path-pair catalog by its signs without multiplicity loss.

  1. def OAI.TwoPointCorrelations.closedTraceFiber line 12
  2. lemma OAI.TwoPointCorrelations.mem_closedTraceFiber line 19
  3. lemma OAI.TwoPointCorrelations.closedTraceFiber_word line 32
  4. theorem OAI.TwoPointCorrelations.sum_closedTraceFiber line 43