OAI/NumberTheory/Ostmann/Tree/QuartetProductFiber.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Tree.Quartet.pairLeaf line 10
2. theorem OAI.Ostmann.Tree.Quartet.pairLeaf_free line 12
3. theorem OAI.Ostmann.Tree.Quartet.pairLeaf_held line 16
4. theorem OAI.Ostmann.Tree.Quartet.pairAssignment_recover line 20
5. theorem OAI.Ostmann.Tree.Quartet.leafProduct_pairLeaf line 31
6. def OAI.Ostmann.Tree.Quartet.crossFiberEquiv line 35
7. theorem OAI.Ostmann.Tree.Quartet.crossFiberEquiv_apply line 58