OAI/NumberTheory/Ostmann/Tree/QuartetCoordinates.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Tree.Quartet.root line 10
  2. def OAI.Ostmann.Tree.Quartet.child line 12
  3. def OAI.Ostmann.Tree.Quartet.ratio line 14
  4. theorem OAI.Ostmann.Tree.Quartet.child_ratio line 16
  5. theorem OAI.Ostmann.Tree.Quartet.shared_pivot_square line 22
  6. theorem OAI.Ostmann.Tree.Quartet.held_square line 29
  7. theorem OAI.Ostmann.Tree.Quartet.root_swap line 35
  8. theorem OAI.Ostmann.Tree.Quartet.ratio_reciprocal_action line 38
  9. theorem OAI.Ostmann.Tree.Quartet.root_reciprocal_action line 42
  10. structure OAI.Ostmann.Tree.Quartet.NodeInput line 46
  11. def OAI.Ostmann.Tree.Quartet.NodeInput.parameters line 61
  12. def OAI.Ostmann.Tree.Quartet.NodeInput.leftFactor line 64
  13. def OAI.Ostmann.Tree.Quartet.NodeInput.rightFactor line 67
  14. def OAI.Ostmann.Tree.Quartet.NodeInput.pivot line 70
  15. def OAI.Ostmann.Tree.Quartet.NodeInput.pivotUnit line 73
  16. def OAI.Ostmann.Tree.Quartet.NodeInput.argument line 75
  17. def OAI.Ostmann.Tree.Quartet.NodeInput.leftArgument line 78
  18. def OAI.Ostmann.Tree.Quartet.NodeInput.rightArgument line 82
  19. theorem OAI.Ostmann.Tree.Quartet.NodeInput.argument_eq line 86
  20. theorem OAI.Ostmann.Tree.Quartet.NodeInput.leftArgument_eq line 94
  21. theorem OAI.Ostmann.Tree.Quartet.NodeInput.rightArgument_eq line 101
  22. theorem OAI.Ostmann.Tree.Quartet.NodeInput.argument_difference line 108
  23. theorem OAI.Ostmann.Tree.Quartet.NodeInput.actual_shared_pivot_square line 113
  24. theorem OAI.Ostmann.Tree.Quartet.NodeInput.actual_child_ratio line 120
  25. theorem OAI.Ostmann.Tree.Quartet.NodeInput.evaluate_eq line 126