OAI/NumberTheory/Ostmann/Construction/ArrangementBoundary.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Transfers along the actual overlap graph

The signed vertex products form a group homomorphism. A slot transfers an arbitrary unit between its two endpoints; connected paths compose transfers.

  1. def OAI.Ostmann.arrangementBoundary line 16
  2. theorem OAI.Ostmann.bulkBlockProduct_mulSingle line 24
  3. theorem OAI.Ostmann.arrangementBoundary_mulSingle line 33
  4. theorem OAI.Ostmann.arrangementBoundary_transfer_adj line 47
  5. theorem OAI.Ostmann.arrangementBoundary_transfer_reachable line 70