OAI/NumberTheory/Ostmann/Tree/CycleSelection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Ostmann.Tree.BalancedSelection line 7
  2. def OAI.Ostmann.Tree.BalancedSelection.of_parallel line 24
  3. def OAI.Ostmann.Tree.BalancedSelection.twist line 51
  4. def OAI.Ostmann.Tree.BalancedSelection.act line 53
  5. theorem OAI.Ostmann.Tree.BalancedSelection.twist_mul line 56
  6. theorem OAI.Ostmann.Tree.BalancedSelection.act_one line 61
  7. theorem OAI.Ostmann.Tree.BalancedSelection.act_mul line 65
  8. theorem OAI.Ostmann.Tree.BalancedSelection.act_positive line 70
  9. theorem OAI.Ostmann.Tree.BalancedSelection.act_negative line 75
  10. theorem OAI.Ostmann.Tree.BalancedSelection.prod_act line 80
  11. theorem OAI.Ostmann.Tree.BalancedSelection.left_product line 89
  12. theorem OAI.Ostmann.Tree.BalancedSelection.right_product line 98