OAI/NumberTheory/Ostmann/Tree/IncidenceCirculation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A balanced leaf action from an incidence-graph cycle

  1. theorem OAI.Ostmann.list_sum_finset_sum line 13
  2. theorem OAI.Ostmann.walk_dart_difference line 20
  3. theorem OAI.Ostmann.walk_dart_reverse_difference line 29
  4. theorem OAI.Ostmann.incidenceDart_exists line 38
  5. def OAI.Ostmann.incidenceDartLabel line 58
  6. theorem OAI.Ostmann.incidenceDartLabel_spec line 62
  7. def OAI.Ostmann.incidenceDartSign line 70
  8. def OAI.Ostmann.incidenceWalkSign line 76
  9. theorem OAI.Ostmann.incidenceWalkSign_block_sum line 81
  10. theorem OAI.Ostmann.incidenceDart_component_difference line 94
  11. theorem OAI.Ostmann.incidenceDart_quartet_difference line 104
  12. theorem OAI.Ostmann.incidenceWalkSign_component_balanced line 114
  13. theorem OAI.Ostmann.incidenceWalkSign_quartet_balanced line 123