OAI/NumberTheory/OrdinaryCorrelations/HighTrace/Block.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.OrdinaryCorrelations.ForestTraversal.Block line 18
2. abbrev OAI.OrdinaryCorrelations.ForestTraversal.Block.walk line 20
3. def OAI.OrdinaryCorrelations.ForestTraversal.cutCount line 23
4. lemma OAI.OrdinaryCorrelations.ForestTraversal.cutCount_nil line 26
5. lemma OAI.OrdinaryCorrelations.ForestTraversal.cutCount_cons line 27
6. lemma OAI.OrdinaryCorrelations.ForestTraversal.cutCount_append line 30
7. def OAI.OrdinaryCorrelations.ForestTraversal.Covers line 34
8. theorem OAI.OrdinaryCorrelations.ForestTraversal.cut_cover line 38