OAI/NumberTheory/OrdinaryCorrelations/HighTrace/TreeDestinationInjective.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.tree_destination_injective line 15
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.tree_destination_nonzero line 26
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.has_incoming_edge line 31
4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.goodOrigins line 54
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.good_origin_data line 57
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.incomingCharges line 63
7. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.returnSteps line 66
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.incomingCharges_image line 68
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.incomingCharges_card line 81
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.incoming_return_disjoint line 88
11. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.source_cutoff_charges line 94