OAI/NumberTheory/Ostmann/Tree/QuartetActions.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Tree.Quartet.scaleLeaf line 10
  2. theorem OAI.Ostmann.Tree.Quartet.leafProduct_scaleLeaf line 12
  3. def OAI.Ostmann.Tree.Quartet.scalePair line 16
  4. theorem OAI.Ostmann.Tree.Quartet.leafProduct_scalePair line 20
  5. def OAI.Ostmann.Tree.Quartet.movePair line 26
  6. theorem OAI.Ostmann.Tree.Quartet.leafProduct_movePair line 29
  7. def OAI.Ostmann.Tree.Quartet.moveCross line 34
  8. theorem OAI.Ostmann.Tree.Quartet.leafProduct_moveCross line 39
  9. def OAI.Ostmann.Tree.Quartet.NodeInput.withLeaves line 47
  10. theorem OAI.Ostmann.Tree.Quartet.NodeInput.argument_withLeaves line 50
  11. theorem OAI.Ostmann.Tree.Quartet.NodeInput.movePair_leftFactor line 55
  12. theorem OAI.Ostmann.Tree.Quartet.NodeInput.movePair_rightFactor line 60
  13. theorem OAI.Ostmann.Tree.Quartet.NodeInput.movePair_ratio line 65
  14. theorem OAI.Ostmann.Tree.Quartet.NodeInput.moveCross_leftFactor line 73
  15. theorem OAI.Ostmann.Tree.Quartet.NodeInput.moveCross_rightFactor line 78
  16. theorem OAI.Ostmann.Tree.Quartet.NodeInput.moveCross_ratio line 83
  17. def OAI.Ostmann.Tree.Quartet.NodeInput.moveSame line 91
  18. theorem OAI.Ostmann.Tree.Quartet.NodeInput.moveSame_factors line 95
  19. theorem OAI.Ostmann.Tree.Quartet.NodeInput.moveSame_pivot line 101