OAI/NumberTheory/Ostmann/Characters/CycleQuartets.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A simple cycle moves at most two leaves in each quartet

  1. theorem OAI.Ostmann.incidenceDart_positive_target line 11
  2. theorem OAI.Ostmann.incidenceDart_negative_source line 19
  3. theorem OAI.Ostmann.exists_dart_of_incidenceWalkSign_ne_zero line 27
  4. theorem OAI.Ostmann.incidenceCycle_positive_unique line 37
  5. theorem OAI.Ostmann.incidenceCycle_negative_unique line 66
  6. theorem OAI.Ostmann.incidenceCycle_quartet_support_card_le_two line 95
  7. structure OAI.Ostmann.BalancedIncidenceCycle line 122

    Source documentation

    The exact combinatorial data required by the quartet projection.

    structure BalancedIncidenceCycle {L C Q : Type*} [Fintype L]
    [DecidableEq L] [DecidableEq C] [DecidableEq Q]
    (component : L → C) (quartet : L → Q) where
…
  8. theorem OAI.Ostmann.exists_balancedIncidenceCycle line 133
  9. theorem OAI.Ostmann.BalancedIncidenceCycle.preserves_component_products line 173
  10. theorem OAI.Ostmann.BalancedIncidenceCycle.preserves_quartet_products line 181