OAI/NumberTheory/OrdinaryCorrelations/HighTrace/SelectedUsed.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData.selected_used line 24
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData.selectedIndex line 27
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData.template line 29
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData.root_relabel line 32
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData.selected_relabel line 33
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData.expression_relabel line 35
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData.formed line 45
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData.root_bound line 49
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData.admissible line 53
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DisconnectedBlockPair.GateSelection.PathData.template_admissible line 72