OAI/NumberTheory/Ostmann/Tree/CycleQuartetActions.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Tree.CycleQuartet.cycleQuartets line 11
  2. theorem OAI.Ostmann.Tree.CycleQuartet.cycleQuartets_nonempty line 13
  3. def OAI.Ostmann.Tree.CycleQuartet.localAct line 16
  4. theorem OAI.Ostmann.Tree.CycleQuartet.localAct_one line 19
  5. theorem OAI.Ostmann.Tree.CycleQuartet.localAct_mul line 24
  6. theorem OAI.Ostmann.Tree.CycleQuartet.bottomLeaves_act line 29
  7. theorem OAI.Ostmann.Tree.CycleQuartet.localAct_product line 35
  8. abbrev OAI.Ostmann.Tree.CycleQuartet.ProductFiber line 48
  9. def OAI.Ostmann.Tree.CycleQuartet.fiberAct line 51
  10. def OAI.Ostmann.Tree.CycleQuartet.fiberMulAction line 55