OAI/NumberTheory/OrdinaryCorrelations/HighTrace/EdgeGraph.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.edgeGraph line 16
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.edgeGraph_adj line 26
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.edgeComponents line 31
4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.componentEdges line 35
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.componentEdges_subset line 39
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.componentEdges_nonempty line 43
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.componentEdges_biUnion line 49
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.component_vertex_class line 59
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.component_edges_disjoint line 71
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.component_vertices_disjoint line 78
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.edgeVertices_biUnion line 86
12. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.subtreeUnionWeight_components line 101
13. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.active_endpoints_iff line 118
14. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.active_graph_exact line 141
15. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.ActiveConnected line 168
16. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.singleton_reachable_endpoints line 174
17. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.no_untagged_fixed_center_good_singleton line 188