OAI/NumberTheory/OrdinaryCorrelations/HighTrace/Nonempty.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.Shape.nonempty line 17
2. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.Shape.grows line 20
3. def OAI.OrdinaryCorrelations.NumericalSubtrees.Shape.topEdge line 23
4. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.Shape.topEdge_mem line 25
5. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.Shape.topEdge_origin line 28
6. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.Shape.unary_edge_eq_topEdge line 31
7. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.Shape.topEdge_le line 39
8. theorem OAI.OrdinaryCorrelations.NumericalSubtrees.selected_shapes_triangular line 42
9. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.prod_eq_pivot_prefix line 47
10. theorem OAI.OrdinaryCorrelations.NumericalSubtrees.selected_prime_product line 62