OAI/NumberTheory/TwoPoint/Walks/ClosedVertexMask.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A closed nonempty word counts a binary vertex mask once per departure, despite the two edge endpoints.

  1. lemma OAI.TwoPointCorrelations.closed_binary_mask_product line 13
  2. theorem OAI.TwoPointCorrelations.closed_masked_scalar_word line 32