OAI/NumberTheory/Ostmann/Tree/CycleQuartetActionsClassification.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Tree.CycleQuartet.position line 8
  2. theorem OAI.Ostmann.Tree.CycleQuartet.position_zero line 10
  3. theorem OAI.Ostmann.Tree.CycleQuartet.position_one line 11
  4. theorem OAI.Ostmann.Tree.CycleQuartet.position_eq_iff line 13
  5. theorem OAI.Ostmann.Tree.CycleQuartet.position_eta line 20
  6. theorem OAI.Ostmann.Tree.CycleQuartet.exists_position line 24
  7. theorem OAI.Ostmann.Tree.CycleQuartet.twoLeafAct_swap line 29
  8. theorem OAI.Ostmann.Tree.CycleQuartet.twoLeafAct_cross line 35
  9. theorem OAI.Ostmann.Tree.CycleQuartet.twoLeafAct_same line 43
  10. inductive OAI.Ostmann.Tree.CycleQuartet.Kind line 51
  11. def OAI.Ostmann.Tree.CycleQuartet.Kind.act line 56
  12. def OAI.Ostmann.Tree.CycleQuartet.classifyPositions line 61
  13. theorem OAI.Ostmann.Tree.CycleQuartet.twoLeafAct_classify line 68
  14. def OAI.Ostmann.Tree.CycleQuartet.kind line 85
  15. theorem OAI.Ostmann.Tree.CycleQuartet.localAct_eq_kind line 88