OAI/NumberTheory/Ostmann/Characters/QuartetIndexCoordinates.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Leaf coordinates within a labeled bottom quartet

  1. def OAI.Ostmann.quartetLeafIndex line 11
  2. def OAI.Ostmann.quartetLeafCoordinates line 16
  3. theorem OAI.Ostmann.quartetLeafCoordinates_index line 21
  4. theorem OAI.Ostmann.quartetLeafIndex_coordinates line 27
  5. theorem OAI.Ostmann.quartetLeafCoordinates_fst line 36
  6. theorem OAI.Ostmann.bottomQuartet_leafIndex line 45
  7. def OAI.Ostmann.quartetLeafIndexEquiv line 49
  8. def OAI.Ostmann.quartetIndexFiberEquiv line 55
  9. theorem OAI.Ostmann.quartetBlockEquiv_read line 66
  10. theorem OAI.Ostmann.sum_bottomQuartet_fiber line 77
  11. theorem OAI.Ostmann.sum_four_treeLeaves line 89